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: Coq(Extraction CRelationClasses) Equations.Init Equations.CoreTactics Equations.Type.Logic Equations.Type.FunctionalExtensionality Equations.Type.Relation Equations.Type.Relation_Properties