fact: Fixpoint xexists (m : t) (i : elt) := match m with | Leaf => false | Node l o r => (o &&& f (rev i)) ||| xexists r i~1 ||| xexists l i~0 end.
imports: Bool PeanoNat BinPos OrderedType OrderedTypeEx FSetInterface