proposition: Lemma conv_term_morph_aux : forall (x x0 : Preterm) (x1 x2 : EnvSubst), x1 <=> x2 -> conv_term x x0 x1 -> conv_term x x0 x2.
proof: Proof. induction x; intros p' E E' EE' convE; inversion convE. constructor 1. rewrite_lr (envSubst_eq_def x y EE'); trivial. constructor 2. constructor 3. apply IHx with (envSubst_lift1 E); trivial. apply envSubst_lift_eq; trivial. constructor 4. apply IHx1 with E; trivial. apply IHx2 with E; trivial. Qed.
imports: CoLoR(RelExtras ListPermutation TermsPos ListUtil ListExtras LogicUtil) Coq(Compare_dec Setoid Morphisms Lia PeanoNat)