proposition: Lemma terms_conv_diff_env_rev : forall M N M' Q, M ~(Q) N -> term M' = term M -> activeEnv M' = activeEnv M -> M' ~(Q) N.
proof: Proof. intros. rewrite <- (envSubst_transp_twice Q). apply terms_conv_sym_aux. apply terms_conv_diff_env with M; trivial. apply terms_conv_sym_aux; trivial. Qed.
imports: CoLoR(RelExtras ListPermutation TermsPos ListUtil ListExtras LogicUtil) Coq(Compare_dec Setoid Morphisms Lia PeanoNat)