fact: Fixpoint split_one (l : list A) : list (A * list A) := match l with | nil => nil (A:=A * list A) | a :: l1 => (a, l1) :: map (fun p : A * list A => (fst p, a :: snd p)) (split_one l1) end.
imports: List ListAux