proposition: Lemma HdRel_list_merge x l1 l2 : HdRel R x l1 → HdRel R x l2 → HdRel R x (list_merge R l1 l2).
proof: Proof. destruct 1 as [|x1 l1 IH1], 1 as [|x2 l2 IH2]; rewrite ?list_merge_cons; simpl; repeat case_decide; auto. Qed.
imports: stdpp(options)