proposition: Theorem binds_map : forall A B x (v : A) (E : gen_env A) (f : A -> B), x ∹ v ⋲ E -> x ∹ (f v) ⋲ (map f E).
proof: Proof. intros A B x v E f Hbind. induction E as [ | E y w IHE ] using env_ind. apply binds_empty in Hbind; inversion Hbind. rewrite map_concat, map_single. apply binds_concat_inv in Hbind. destruct Hbind as [ Hbind | [ Hnotin Hbind ] ]. apply binds_single_inv in Hbind. destruct Hbind; subst. apply binds_concat_r. apply binds_single; auto. apply binds_concat_l; auto. apply notin_single. apply notin_single_inv in Hnotin; auto. Qed.
imports: Utf8 Equalities CoreGenericEnv