proposition: Lemma mapo_mapsto m x v' : (mapo f m)@x ↦ v' -> exists y v, y == x /\ m@x ↦ v /\ f y v = Some v'.
proof: Proof. unfold mapo. rewrite treeify_mapsto, mapoL_mapsto, InA_nil; auto. intros [(y & v & E & IN & Hf)|[ ]]. rewrite rev_bindings_rev, <-In_rev in IN. exists y, v. repeat split; auto. apply bindings_spec1. rewrite InA_alt. exists (y, v). split; autom. Qed.
imports: Coq(Bool BinPos Pnat Setoid SetoidList PeanoNat) Coq(Orders OrdersFacts OrdersLists) MMaps(Utils Interface OrdList GenTree)