proposition: Lemma AccR_morph_aux : forall x1 x2 : Term, x1 ~ x2 -> AccR x1 -> AccR x2.
proof: Proof. intros M M' M'M AccM'; unfold AccR. apply Acc_homo with (x := M) (R := transp R) (morphism := terms_conv); trivial. unfold transp; intros x y x' x'x xy. destruct (R_conv_to (M':=x') xy (terms_conv_sym x'x)) as [y' [x'y' yy']]. exists y'; trivial. apply terms_conv_sym; trivial. Qed.
imports: CoLoR(RelExtras ListExtras PairLex Horpo LogicUtil AccUtil) Coq(Setoid Morphisms Basics)