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