Lemma isweqdnitocompl ( n : nat ) ( i : ⟦S n⟧ ) : isweq ( dnitocompl n i ). Proof. intros jni. assert ( w := samehfibers ( dnitocompl n i ) _ ( isinclpr1compl_ne _ i _ ) jni ) ; simpl in w. apply (iscontrweqb w). apply iscontrhfiberdni. exact (pr2 jni). Defined.
Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.MoreFoundations.DecidablePropositions. Require Import UniMath.MoreFoundations.NegativePropositions.