proposition: Lemma in_leaf {elt} y : y ∈ (@Leaf elt) <-> False.
proof: Proof. unfold In. setoid_rewrite leaf_mapsto. firstorder. Qed.
imports: Coq(Bool Arith BinInt FunInd) Coq(Orders OrdersFacts OrdersLists) MMaps(Comparisons Interface OrdList)