proposition: Lemma merge_Permutation l1 l2 : list_merge R l1 l2 ≡ₚ l1 ++ l2.
proof: Proof. revert l2. induction l1 as [|x1 l1 IH1]; intros l2; induction l2 as [|x2 l2 IH2]; rewrite ?list_merge_cons; simpl; repeat case_decide; auto. - by rewrite (right_id_L [] (++)). - by rewrite IH2, Permutation_middle. Qed.
imports: stdpp(options)