fact: Fixpoint subsetl (subset_l1 : tree -> bool) x1 s2 : bool := match s2 with | Leaf => false | Node _ l2 x2 r2 => match X.compare x1 x2 with | Eq => subset_l1 l2 | Lt => subsetl subset_l1 x1 l2 | Gt => mem x1 r2 &&& subset_l1 s2 end end.
imports: Orders OrdersFacts MSetInterface PeanoNat