proposition: Lemma terms_conv_criterion_strong : forall M N, activeEnv M = activeEnv N -> term M = term N -> M ~ N.
proof: Proof. intros. exists (idEnvSubst (length (env M))). constructor. rewrite <- H0. apply conv_term_refl. intros p q pq. inversion pq. intro. rewrite H; rewrite H1; split; trivial. Qed.
imports: CoLoR(RelExtras ListPermutation TermsPos ListUtil ListExtras LogicUtil) Coq(Compare_dec Setoid Morphisms Lia PeanoNat)