proposition: Lemma split_beyond : forall E k n p, p < k -> length E <= p -> (initialSeg E k ++ copy n None ++ finalSeg E k) |= p :! .
proof: Proof. intros; unfold VarUD. rewrite nth_app_right; autorewrite with datatypes. destruct (le_gt_dec n (p - Nat.min k (length E))). rewrite nth_app_right; autorewrite with datatypes; trivial. left; apply nth_beyond; autorewrite with datatypes; trivial. simpl; lia. rewrite nth_app_left; autorewrite with datatypes; try_solve. set (w := Nat.le_min_r k (length E)); lia. Qed.
imports: CoLoR(RelExtras ListExtras TermsLifting LogicUtil OptUtil) Coq(Arith Setoid Morphisms Lia)