proposition: Lemma conv_term_sym : forall PtL PtR S, conv_term PtL PtR S -> conv_term PtR PtL (envSubst_transp S).
proof: Proof. intros. induction H. constructor 1; destruct S; trivial. constructor 2. constructor 3. rewrite <- (envSubst_transp_lift S); trivial. constructor 4; trivial. Qed.
imports: CoLoR(RelExtras ListPermutation TermsPos ListUtil ListExtras LogicUtil) Coq(Compare_dec Setoid Morphisms Lia PeanoNat)