proposition: Lemma conv_env_refl : forall M, conv_env M M (idEnvSubst (length (env M))).
proof: Proof. intros E x y xy A; split; inversion xy; rewrite H; trivial. Qed.
imports: CoLoR(RelExtras ListPermutation TermsPos ListUtil ListExtras LogicUtil) Coq(Compare_dec Setoid Morphisms Lia PeanoNat)