proposition: Lemma presubst_beyond Pt i j G : j >= length G -> presubst_aux (prelift Pt j) i G = prelift Pt j.
proof: Proof. intro. unfold prelift. apply presubst_beyond_aux. lia. intros; lia. Qed.
imports: CoLoR(RelExtras ListPermutation TermsConv ListUtil ListExtras LogicUtil) Coq(Arith Lia)