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