proposition: Lemma presubst_prelift_comm Pt i G : presubst (prelift Pt i) (copy i None ++ lift_subst G i) = prelift (presubst Pt G) i.
proof: Proof. unfold presubst, prelift. replace i with (0 + i); trivial. rewrite presubst_prelift_aux; trivial. Qed.
imports: CoLoR(RelExtras ListPermutation TermsConv ListUtil ListExtras LogicUtil) Coq(Arith Lia)