fact: Fixpoint equal (s : t) : t -> bool := fun s' : t => match s, s' with | nil, nil => true | x :: l, x' :: l' => match X.compare x x' with | Eq => equal l l' | _ => false end | _, _ => false end.
imports: MSetInterface OrdersFacts OrdersLists