proposition: Lemma conv_env_trans : forall M N P mn np, conv_env M N mn -> conv_env N P np -> conv_env M P (envSubst_compose mn np).
proof: Proof. intros; destruct mn; destruct np. intros x y xy A; destruct xy as [z [xz zy]]. split; intro. Set Firstorder Depth 6. set (hint := H x z xz); fo. set (hint := H0 z y zy); fo. Qed.
imports: CoLoR(RelExtras ListPermutation TermsPos ListUtil ListExtras LogicUtil) Coq(Compare_dec Setoid Morphisms Lia PeanoNat)