proposition: Lemma irrefl z : ¬ (z < z).
proof: Proof. intro l. simple refine (pr1 (strongly_from_weakly_well_founded wwf_lt (λ t, ¬ (z=t)) _) z (idpath z)). intros x h e. induction e. exact (h z l (idpath z)). Defined.
imports: UniMath.Foundations.All UniMath.MoreFoundations.Propositions UniMath.MoreFoundations.Univalence