proposition: Lemma bindings_nil m : bindings m = nil <-> is_empty m = true.
proof: Proof. unfold bindings. now rewrite xbindings_nil. Qed.
imports: Coq(Bool PeanoNat BinPos Orders OrdersEx OrdersLists) MMaps(Utils Comparisons Interface)