proposition: Lemma presubst_lift_beyond : forall Pt G m n i (W := prelift_aux n Pt m), m <= i -> m + n >= i + length G -> presubst W (copy i None ++ G) = W.
proof: Proof. induction Pt; intros G m n i W m_c mn_c; unfold W, presubst; simpl. destruct (le_gt_dec m x); simpl. rewrite nth_beyond; trivial. rewrite length_app. rewrite copy_length. lia. rewrite nth_app_left. destruct (nth_error_In (copy i (@None Term)) x) as [ [ss ss_nth] | sn]. rewrite ss_nth. rewrite (copy_in i None ss (nth_some_in _ _ ss_nth)); trivial. rewrite sn; trivial. autorewrite with datatypes using lia. trivial. rewrite subst_lift_subst; simpl. rewrite lift_subst_distr. rewrite lift_empty_subst. rewrite app_comm_cons. rewrite copy_cons. rewrite (IHPt (lift_subst G 1) (S m) n (S i)); trivial. lia. rewrite (length_lift_subst G 1). lia. fold (presubst (prelift_aux n Pt1 m) (copy i None ++ G)). rewrite IHPt1; trivial. fold (presubst (prelift_aux n Pt2 m) (copy i None ++ G)). rewrite IHPt2; trivial. Qed.
imports: CoLoR(RelExtras ListPermutation TermsConv ListUtil ListExtras LogicUtil) Coq(Arith Lia)