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