proposition: Lemma terms_conv_criterion : forall M N, env M [<->] env N -> term M = term N -> M ~ N.
proof: Proof. intros M N MNenv MNterm; exists (compEnvSubst MNenv); constructor. apply conv_term_comp_refl; trivial. intros x y xy A. inversion xy; rewrite H. rewrite (equiv_term_activeEnv M N); trivial. split; trivial. Qed.
imports: CoLoR(RelExtras ListPermutation TermsPos ListUtil ListExtras LogicUtil) Coq(Compare_dec Setoid Morphisms Lia PeanoNat)