proposition: Lemma varUD_hole : forall E i, (initialSeg E i ++ None :: finalSeg E (S i)) |= i :!.
proof: Proof. intros. destruct (lt_eq_lt_dec (length E) i) as [[iE | iE] | iE]. left. apply nth_beyond. autorewrite with datatypes using simpl; try lia. right. rewrite nth_app_right; autorewrite with datatypes; rewrite iE. apply Nat.min_case; replace (i - i) with 0; solve [trivial | lia]. auto with arith. right. rewrite nth_app_right; autorewrite with datatypes; auto with arith. replace (i - Nat.min i (length E)) with 0; trivial. rewrite Nat.min_l; lia. Qed.
imports: CoLoR(RelExtras ListExtras TermsLifting LogicUtil OptUtil) Coq(Arith Setoid Morphisms Lia)