fact: Fixpoint subset s s' := match s, s' with | nil, _ => true | x :: l, x' :: l' => match X.compare x x' with | Lt => false | Eq => subset l l' | Gt => subset s l' end | _, _ => false end.
imports: MSetInterface OrdersFacts OrdersLists