proposition: Lemma Acc_mimic : forall x (P: relation A), Acc R x -> mimic P -> forall x', P x x' -> Acc R x'.
proof: Proof. induction 1. intros mim x' Pxx'. constructor. intros y' Ry'x'. unfold mimic in mim. destruct (mim x x' Pxx' y' Ry'x') as [y Ryx Pyy']. apply H0 with y; trivial. Qed.
imports: Coq(Morphisms Basics) CoLoR(LogicUtil RelUtil) Coq(List)