proposition: Lemma Acc_homo : forall x, Acc R x -> forall x', morphism x x' -> Acc T x'.
proof: Proof. induction 1. intros x' x0x'. constructor. intros w Twx'. destruct (comp x0x' Twx') as [x1 Rx x1w]. eapply H0; eauto. Qed.
imports: Coq(Morphisms Basics) CoLoR(LogicUtil RelUtil) Coq(List)