fact: Fixpoint sort_aux2 (l:list (list A)) (b:nat) {struct b} : list A := match b with | O => nil (A:=A) | S b' => match l with | nil => nil (A:=A) | l' :: nil => l' | _ => sort_aux2 (sort_aux1 l) b' end end.
imports: List Lia