proposition: Lemma conv_env_empty : forall M N, conv_env M N emptyEnvSubst.
proof: Proof. intros M N x y F; try_solve. Qed.
imports: CoLoR(RelExtras ListPermutation TermsPos ListUtil ListExtras LogicUtil) Coq(Compare_dec Setoid Morphisms Lia PeanoNat)