proposition: Lemma map_option_2 : forall (m:t elt)(x:key), In x (map_option f m) -> exists d, MapsTo x d m /\ f x d <> None.
proof: Proof. intros m; functional induction (map_option f m); simpl; auto; intros. - inversion H. - rewrite join_in in H; destruct H as [H|[H|H]]. + exists d; split; auto; rewrite (f_compat d H), e0; discriminate. + destruct (IHt _ H) as (d0 & ? & ?); exists d0; auto. + destruct (IHt0 _ H) as (d0 & ? & ?); exists d0; auto. - rewrite concat_in in H; destruct H as [H|H]. + destruct (IHt _ H) as (d0 & ? & ?); exists d0; auto. + destruct (IHt0 _ H) as (d0 & ? & ?); exists d0; auto. Qed.
imports: FunInd FMapInterface FMapList ZArith Int