proposition: Lemma Sorted_merge_sort_aux `{!Total R} st l : merge_stack_Sorted st → Sorted R (merge_sort_aux R st l).
proof: Proof. revert st. induction l; simpl; auto using Sorted_merge_stack, Sorted_merge_list_to_stack. Qed.
imports: stdpp(options)