proposition: Lemma Acc_eq_rel : forall A (R S : relation A) x, (forall a b, R a b <-> S a b) -> Acc R x -> Acc S x.
proof: Proof. induction 2. constructor. intros z Szx; apply H1. exact (proj2 (H z x) Szx). Qed.
imports: Coq(Morphisms Basics) CoLoR(LogicUtil RelUtil)