fact: Fixpoint split_all (A : Type) (l : list A) : list (A * (list A * list A)) := match l with | nil => @nil _ | a :: l => (a,(@nil _, l)) :: (map (fun bl' => match bl' with (b,(l',l'')) => (b, (a :: l',l'')) end) (split_all l)) end.
imports: Coq(List Relations Arith Setoid Morphisms FunInd) CoLoR(decidable_set more_list equiv_list)