proposition: Lemma terms_conv_sym : forall M N, M ~ N -> N ~ M.
proof: Proof. intros M N MN; destruct MN. exists (envSubst_transp x). apply terms_conv_sym_aux; trivial. Qed.
imports: CoLoR(RelExtras ListPermutation TermsPos ListUtil ListExtras LogicUtil) Coq(Compare_dec Setoid Morphisms Lia PeanoNat)