proposition: Lemma in_node {elt} l x (e:elt) r h y : y ∈ (Node h l x e r) <-> y ∈ l \/ y == x \/ y ∈ r.
proof: Proof. unfold In. setoid_rewrite node_mapsto. firstorder. exists e. intuition. Qed.
imports: Coq(Bool Arith BinInt FunInd) Coq(Orders OrdersFacts OrdersLists) MMaps(Comparisons Interface OrdList)