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