proposition: Lemma tc_prop_iff A (R E : rel A) : Equivalence E -> Proper (E ==> E ==> iff) R -> Proper (E ==> E ==> iff) (clos_trans R).
proof: Proof. intros E_eq R_prop. apply prop_rel_sym; class. apply tc_prop; class. intros x x' xx' y y' yy' xy. rewrite <- xx', <- yy'. hyp. Qed.
imports: Coq(Setoid Basics Morphisms List Lia) CoLoR(LogicUtil)