proposition: Lemma varD_hole_rev : forall E i j A, i <> j -> (initialSeg E i ++ None :: finalSeg E (S i)) |= j := A -> E |= j := A.
proof: Proof. unfold VarD; intros. destruct (lt_eq_lt_dec i j) as [[ij | ij] | ij]. assert (length E > i). apply varD_hole_env_length_j_ge_i with j A; auto with arith. rewrite nth_app_right in H0; autorewrite with datatypes. replace (length (initialSeg E i)) with i in H0. 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 (H2 (option SimpleType) (finalSeg E (S i)) None (j - i)) in H0. replace j with (S i + pred (j - i)). rewrite <- nth_finalSeg_nth; trivial. lia. lia. autorewrite with datatypes; rewrite Nat.min_l; trivial; lia. rewrite Nat.min_l; trivial; lia. lia. rewrite nth_app_left in H0; autorewrite with datatypes. apply initialSeg_prefix with i; trivial. assert (Nat.min i (length E) > j). rewrite Nat.min_comm. apply Nat.min_case; trivial. apply varD_hole_env_length with i A; trivial. lia. Qed.
imports: CoLoR(RelExtras ListExtras TermsLifting LogicUtil OptUtil) Coq(Arith Setoid Morphisms Lia)