proposition: Lemma conv_env_sym : forall M N mn, conv_env M N mn -> conv_env N M (envSubst_transp mn).
proof: Proof. intros i j; intros; destruct mn; fo. Qed.
imports: CoLoR(RelExtras ListPermutation TermsPos ListUtil ListExtras LogicUtil) Coq(Compare_dec Setoid Morphisms Lia PeanoNat)