proposition: Lemma conv_term_trans : forall M N P mn np, conv_term M N mn -> conv_term N P np -> conv_term M P (envSubst_compose mn np).
proof: Proof. intros M N P mn np MN NP; revert P np NP; induction MN; intros P np NP; destruct P; inversion NP. constructor 1; simpl. destruct S; destruct np; exists y; split; trivial. constructor 2. constructor 3. rewrite (envSubst_lift_compose S np). apply IHMN; trivial. constructor 4. apply IHMN1; trivial. apply IHMN2; trivial. Qed.
imports: CoLoR(RelExtras ListPermutation TermsPos ListUtil ListExtras LogicUtil) Coq(Compare_dec Setoid Morphisms Lia PeanoNat)