proposition: Lemma Acc_iso : iso x z -> Acc R x -> Acc T z.
proof: Proof. intros iso_x_z Acc_x; generalize z iso_x_z; clear iso_x_z z. induction Acc_x as [x Acc_x Hind]. intros z iso_x_z. constructor. intros z' T_z'_z. elim (iso_comp iso_x_z T_z'_z). intros x' Rx' iso_x'_z'. apply Hind with x'; hyp. Qed.
imports: Coq(Morphisms Basics) CoLoR(LogicUtil RelUtil) Coq(List)