proposition: Lemma terms_eq_conv : forall M N, M = N -> M ~ N.
proof: Proof. intros; exists (idEnvSubst (length (env M))); rewrite H. constructor. apply conv_term_refl. apply conv_env_refl. Qed.
imports: CoLoR(RelExtras ListPermutation TermsPos ListUtil ListExtras LogicUtil) Coq(Compare_dec Setoid Morphisms Lia PeanoNat)