proposition: Lemma presubst_beyond_aux : forall Pt i j k G, j + k >= length G -> (forall p, p < k -> G |-> p/-) -> presubst_aux (prelift_aux j Pt k) i G = prelift_aux j Pt k.
proof: Proof. induction Pt; unfold prelift; intros; simpl. destruct (le_gt_dec k x); simpl. rewrite nth_beyond; trivial. lia. destruct (H0 x). lia. rewrite H1; trivial. rewrite H1; trivial. trivial. assert (presubst_aux (prelift_aux j Pt (S k)) (S i) (None :: G) = prelift_aux j Pt (S k)). apply IHPt. simpl; lia. intros. destruct p. constructor 2; trivial. apply (H0 p); lia. congruence. rewrite IHPt1; trivial. rewrite IHPt2; trivial. Qed.
imports: CoLoR(RelExtras ListPermutation TermsConv ListUtil ListExtras LogicUtil) Coq(Arith Lia)