proposition: Lemma node_mapsto {elt} l x (e:elt) r h y v : (Node h l x e r)@y ↦ v <-> l@y ↦ v \/ (y == x /\ v = e) \/ r@y ↦ v.
proof: Proof. intuition_m; subst; auto with map. Qed.
imports: Coq(Bool Arith BinInt FunInd) Coq(Orders OrdersFacts OrdersLists) MMaps(Comparisons Interface OrdList)