proposition: Lemma varD_hole_env_length : forall E i j A, (initialSeg E i ++ None :: finalSeg E (S i)) |= j := A -> length E > j.
proof: Proof. unfold VarD; intros. destruct (le_lt_dec (Nat.min i (length E)) j). rewrite (@nth_app_right (option SimpleType) (initialSeg E i) (None :: finalSeg E (S i)) j) in H. rewrite initialSeg_length in H. destruct (le_gt_dec (length E) i); trivial. rewrite Nat.min_r in H; trivial. rewrite (finalSeg_empty E (k := S i)) in H. destruct (j - length E); try destruct n; try_solve. lia. assert (forall (A : Type) l (a: A) i, i > 0 -> nth_error (a::l) i = nth_error l (pred i)). intros; destruct i0; try_solve. lia. rewrite H0 in H. set (w := finalSeg_nth_idx E (S i) (pred (j - Nat.min i (length E))) H). rewrite Nat.min_l in w; lia. destruct (j - Nat.min i (length E)); try_solve. lia. autorewrite with datatypes; trivial. rewrite nth_app_left in H; autorewrite with datatypes; trivial. set (w := Nat.le_min_r i (length E)); lia. Qed.
imports: CoLoR(RelExtras ListExtras TermsLifting LogicUtil OptUtil) Coq(Arith Setoid Morphisms Lia)