proposition: Lemma wf_irrefl : forall A (R : relation A), well_founded R -> Irreflexive R.
proof: Proof. intros A R wf x. induction (wf x). intro n. eapply H0. apply n. hyp. Qed.
imports: Coq(Morphisms Basics) CoLoR(LogicUtil RelUtil) Coq(List)