proposition: Lemma env_hole_subset : forall E i, envSubset (initialSeg E i ++ None :: finalSeg E (S i)) E.
proof: Proof. intros; intros j A D. destruct (eq_nat_dec i j). rewrite e in D. assert (length (initialSeg E j) = j). autorewrite with datatypes. apply Nat.min_l. assert (length E > j). apply varD_hole_env_length_j_ge_i with j A; trivial. lia. lia. unfold VarD in D. rewrite nth_app_right in D. replace (j - length (initialSeg E j)) with 0 in D. inversion D. rewrite H; lia. lia. apply varD_hole_rev with i; trivial. Qed.
imports: CoLoR(RelExtras ListExtras TermsLifting LogicUtil OptUtil) Coq(Arith Setoid Morphisms Lia)