proposition: Lemma terms_conv_activeEnv_sub : forall M M' N N' Q, M ~(Q) M' -> envSubset (activeEnv N) (activeEnv M) -> N ~(Q) N' -> envSubset (activeEnv N') (activeEnv M').
proof: Proof. intros; intros x A N'x. destruct (terms_conv_activeEnv_rev H1 N'x). apply (proj1 ((proj2 H) x0 x H2 A)). apply H0. apply (proj2 ((proj2 H1) x0 x H2 A)); trivial. Qed.
imports: CoLoR(RelExtras ListPermutation TermsPos ListUtil ListExtras LogicUtil) Coq(Compare_dec Setoid Morphisms Lia PeanoNat)