fact: Fixpoint flatten_stack (stack : list (option (list t))) := match stack with | [] => [] | None :: stack' => flatten_stack stack' | Some l :: stack' => l ++ flatten_stack stack' end.
imports: List Setoid Permutation Sorted Orders