proposition: Lemma ok_update_one : forall x v E, ok E -> ok (E [x <- v]).
proof: Proof. intros x v E Hok. induction E as [ | E y w ] using env_ind. rewrite update_one_empty. apply ok_nil. inversion Hok as [ | z u F Hok2 ]; subst. destruct Hok2. destruct (eq_keys_dec x y) as [ Heq | Hneq ]; subst. rewrite update_one_concat_r; [ | apply belongs_single; auto ]. rewrite update_one_single; auto. apply ok_cons; auto. rewrite update_one_concat_l; [ | apply notin_single; auto ]. apply ok_cons. split; auto. apply notin_update_one; auto. Qed.
imports: Utf8 Equalities