fact: Fixpoint merge_list_to_stack (st : stack) (l : list A) : stack := match st with | [] => [Some l] | None :: st => Some l :: st | Some l' :: st => None :: merge_list_to_stack st (list_merge l' l) end.
imports: stdpp(options)