proposition: Lemma list_merge_cons x1 x2 l1 l2 : list_merge R (x1 :: l1) (x2 :: l2) = if decide (R x1 x2) then x1 :: list_merge R l1 (x2 :: l2) else x2 :: list_merge R (x1 :: l1) l2.
proof: Proof. done. Qed.
imports: stdpp(options)