fact: Fixpoint union (m m': t) : t := match m with | Leaf => m' | Node l o r => match m' with | Leaf => m | Node l' o' r' => Node (union l l') (o||o') (union r r') end end.
imports: Bool PeanoNat BinPos Orders OrdersEx MSetInterface