proposition: Lemma varD_hole_env_length_j_ge_i : forall E i j A, j >= i -> (initialSeg E i ++ None :: finalSeg E (S i)) |= j := A -> length E > i.
proof: Proof. intros; set (w := varD_hole_env_length E i H0); lia. Qed.
imports: CoLoR(RelExtras ListExtras TermsLifting LogicUtil OptUtil) Coq(Arith Setoid Morphisms Lia)