proposition: Lemma neghfiberdi (i : nat) : ¬ (hfiber (di i) i).
proof: Proof. intros hf. unfold di in hf. induction hf as [ j e ]. induction (natlthorgeh j i) as [ l | g ]. induction e. apply (isirreflnatlth _ l). induction e in g. apply (negnatgehnsn _ g). Defined.
imports: UniMath.Foundations.Sets