proposition: Lemma Acc_rtc : forall x y, clos_refl_trans R x y -> Acc R y -> Acc R x.
proof: Proof. induction 1. intro. eapply Acc_inv. apply H0. hyp. auto. intro. apply IHclos_refl_trans1. apply IHclos_refl_trans2. hyp. Qed.
imports: Coq(Morphisms Basics) CoLoR(LogicUtil RelUtil)