proposition: Lemma cardinal_spec m : cardinal m = length (bindings m).
proof: Proof. unfold bindings. rewrite xbindings_length. simpl. symmetry. apply Nat.add_0_r. Qed.
imports: Coq(Bool PeanoNat BinPos Orders OrdersEx OrdersLists) MMaps(Utils Comparisons Interface)