fact: Fixpoint union (s : t) : t -> t := match s with | nil => fun s' => s' | x :: l => (fix union_aux (s' : t) : t := match s' with | nil => s | x' :: l' => match X.compare x x' with | Lt => x :: union l s' | Eq => x :: union l l' | Gt => x' :: union_aux l' end end) end.
imports: MSetInterface OrdersFacts OrdersLists