proposition: Lemma mapo_find m x `{!Ok m} : exists y, y == x /\ find x (mapo f m) = obind (find x m) (f y).
proof: Proof. assert (Ok (mapo f m)) by ok. destruct (@mapoL_find (rev_bindings m) nil x) as (y & Hy & EQ). - rewrite rev_bindings_rev, rev_involutive; now apply bindings_spec2. - exists y; split; auto. unfold mapo in *. rewrite <- !findL_find; auto. rewrite treeify_bindings, EQ. simpl. clear EQ. rewrite rev_bindings_rev, rev_involutive. now destruct obind. Qed.
imports: Coq(Bool BinPos Pnat Setoid SetoidList PeanoNat) Coq(Orders OrdersFacts OrdersLists) MMaps(Utils Interface OrdList GenTree)