Lemma irrefl z : ¬ (z < z). 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.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.Univalence.