proposition: Lemma well_founded_irreflexive {A} {R : Relation A} {wfR : well_founded R} : forall x y : A, R x y -> x = y -> Empty.
proof: Proof. intros x y Ryy. intros e. destruct e. red in wfR. induction (wfR x) as [y accy IHy]. apply (IHy _ Ryy Ryy). Qed.
imports: Equations.Init Equations.CoreTactics Equations.HoTT.Logic Equations.HoTT.Relation Equations.HoTT.Relation_Properties HoTT.Basics.Tactics