proposition: Lemma mapo_in m x : x ∈ (mapo f m) -> exists y d, y == x /\ MapsTo x d m /\ f y d <> None.
proof: Proof. functional induction (mapo f m); simpl; auto. - intuition_in. - rewrite join_in; intros [H|[H|H]]. + exists x0, d. do 2 (split; autom). congruence. + destruct (IHt0 H) as (y & e & ? & ? & ?). exists y, e. autom. + destruct (IHt1 H) as (y & e & ? & ? & ?). exists y, e. autom. - rewrite concat_in; intros [H|H]. + destruct (IHt0 H) as (y & e & ? & ? & ?). exists y, e. autom. + destruct (IHt1 H) as (y & e & ? & ? & ?). exists y, e. autom. Qed.
imports: Coq(Bool PeanoNat BinInt FunInd Int) Coq(Orders OrdersFacts OrdersLists) MMaps(Utils Interface OrdList GenTree)