proposition: Lemma well_founded_antisym@{i j} {A : Type@{i}} {R : relation@{i j} A}{wfR : well_founded R} : forall x y : A, R x y -> R y x -> Empty.
proof: Proof. intros x y Rxy Ryx. red in wfR. induction (wfR y) as [y accy IHy] in x, Rxy, Ryx. specialize (IHy _ Rxy). apply (IHy _ Ryx Rxy). Qed.
imports: Coq(Extraction CRelationClasses) Equations.Init Equations.CoreTactics Equations.Type.Logic Equations.Type.FunctionalExtensionality Equations.Type.Relation Equations.Type.Relation_Properties