proposition: Lemma conv_term_lifted : forall M N Q, conv_term M N Q -> conv_term (prelift M 1) (prelift N 1) (envSubst_lift1 Q).
proof: Proof. intros. unfold prelift. apply conv_term_lifted_aux; trivial. intros; lia. Qed.
imports: CoLoR(RelExtras ListPermutation TermsPos ListUtil ListExtras LogicUtil) Coq(Compare_dec Setoid Morphisms Lia PeanoNat)