proposition: Lemma terms_conv_trans : forall M N P, M ~ N -> N ~ P -> M ~ P.
proof: Proof. intros M N P MN NP. destruct MN; destruct NP. inversion H; inversion H0. exists (envSubst_compose x x0); constructor. apply conv_term_trans with (term N); trivial. apply conv_env_trans with N; trivial. Qed.
imports: CoLoR(RelExtras ListPermutation TermsPos ListUtil ListExtras LogicUtil) Coq(Compare_dec Setoid Morphisms Lia PeanoNat)