proposition: Lemma Sorted_merge_list_to_stack `{!Total R} st l : merge_stack_Sorted st → Sorted R l → merge_stack_Sorted (merge_list_to_stack R st l).
proof: Proof. intros Hst. revert l. induction Hst; repeat constructor; naive_solver auto using Sorted_list_merge. Qed.
imports: stdpp(options)