proposition: Lemma terms_conv_with_morph_aux : forall x1 x2 : EnvSubst, x1 <=> x2 -> forall x x0 : Term, x ~ (x1)x0 -> x ~ (x2)x0.
proof: Proof. intros; inversion H0. constructor; rewrite <- H; trivial. Qed.
imports: CoLoR(RelExtras ListPermutation TermsPos ListUtil ListExtras LogicUtil) Coq(Compare_dec Setoid Morphisms Lia PeanoNat)