proposition: Lemma varD_hole : forall E i j A, i <> j -> E |= j := A -> (initialSeg E i ++ None :: finalSeg E (S i)) |= j := A.
proof: Proof. unfold VarD; intros. set (iE := nth_some E j H0). destruct (lt_eq_lt_dec i j) as [[ij | ij] | ij]. rewrite nth_app_right; autorewrite with datatypes; rewrite Nat.min_l; try lia. replace (j - i) with (S (j - S i)); try lia. simpl; rewrite nth_finalSeg_nth. replace (S i + (j - S i)) with j; [trivial | lia]. lia. rewrite nth_app_left; autorewrite with datatypes; trivial. apply Nat.min_case; trivial. Qed.
imports: CoLoR(RelExtras ListExtras TermsLifting LogicUtil OptUtil) Coq(Arith Setoid Morphisms Lia)