proposition: Lemma terms_conv_sym_aux : forall M N Q, M ~(Q) N -> N ~(envSubst_transp Q) M.
proof: Proof. intros. constructor. apply conv_term_sym; fo. apply conv_env_sym; fo. Qed.
imports: CoLoR(RelExtras ListPermutation TermsPos ListUtil ListExtras LogicUtil) Coq(Compare_dec Setoid Morphisms Lia PeanoNat)