proposition: Lemma terms_conv_refl : forall M, M ~ M.
proof: Proof. intro M. exists (idEnvSubst (length (env M))); 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)