proposition: Lemma merge_sort_aux_Permutation st l : merge_sort_aux R st l ≡ₚ merge_stack_flatten st ++ l.
proof: Proof. revert st. induction l as [|?? IH]; simpl; intros. - by rewrite (right_id_L [] (++)), merge_stack_Permutation. - rewrite IH, merge_list_to_stack_Permutation; simpl. by rewrite Permutation_middle. Qed.
imports: stdpp(options)