proposition: Lemma ok_map_inv : forall E f, ok (map f E) -> ok E.
proof: Proof. intros E f Hok. induction E using env_ind. apply ok_nil. rewrite map_concat in Hok. rewrite map_single in Hok. 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; auto. Qed.
imports: Utf8 Equalities