proposition: Lemma ok_map : forall E f, ok E -> ok (map f E).
proof: Proof. intros E f Hok. induction E using env_ind. rewrite map_empty. apply ok_nil. rewrite map_concat. rewrite map_single. apply ok_cons. inversion Hok as [ | y w F Hok2 ]; subst. destruct Hok2 as [ Hok2 Hnotin ]. split; auto. intro Hin. elim Hnotin. apply belongs_map_inv with f; auto. Qed.
imports: Utf8 Equalities