proposition: Lemma clos_trans_aeq R : Proper (aeq ==> aeq ==> impl) R -> Proper (aeq ==> aeq ==> impl) (R!).
proof: Proof. intros R_aeq t t' tt' u u' uu' tu. revert t u tu t' tt' u' uu'; induction 1; intros t' tt' u' uu'. apply t_step. rewrite <- tt', <- uu'. hyp. trans y; firstorder auto with crelations. Qed.
imports: Coq(Wf_nat Morphisms Basics Equivalence) CoLoR(BoolUtil RelUtil LogicUtil SN VecUtil NatUtil VecOrd)