fact: Fixpoint cardinal (m : t A) : nat := match m with | Leaf => 0%nat | Node l None r => (cardinal l + cardinal r)%nat | Node l (Some _) r => S (cardinal l + cardinal r) end.
imports: Bool OrderedType ZArith OrderedType OrderedTypeEx FMapInterface