proposition: Lemma well_founded_antisym {A} {R : A -> A -> Prop}{wfR : WellFounded R} : forall x y : A, R x y -> R y x -> False.
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: Program Equations.Prop.EqDecInstances Equations.Prop.Equations