proposition: Lemma merge_list_to_stack_Permutation st l : merge_stack_flatten (merge_list_to_stack R st l) ≡ₚ l ++ merge_stack_flatten st.
proof: Proof. revert l. induction st as [|[l'|] st IH]; intros l; simpl; auto. by rewrite IH, merge_Permutation, (assoc_L _), (comm (++) l). Qed.
imports: stdpp(options)