fact: Fixpoint list_merge (l1 : list A) : list A → list A := fix list_merge_aux l2 := match l1, l2 with | [], _ => l2 | _, [] => l1 | x1 :: l1, x2 :: l2 => if decide (R x1 x2) then x1 :: list_merge l1 (x2 :: l2) else x2 :: list_merge_aux l2 end.
imports: stdpp(options)