fact: Fixpoint union_list l1 : list elt -> list elt -> list elt := match l1 with | nil => @rev_append _ | x::l1' => fix union_l1 l2 acc := match l2 with | nil => rev_append l1 acc | y::l2' => match X.compare x y with | Eq => union_list l1' l2' (x::acc) | Lt => union_l1 l2' (y::acc) | Gt => union_list l1' l2 (x::acc) end end end.
imports: Bool List BinPos Pnat Setoid SetoidList PeanoNat