fact: Fixpoint addInAllLocations(A : Type)(a : A)(ls : list A) := match ls with | nil => (a :: nil) :: nil | a' :: ls' => (a :: ls) :: map (fun x => a' :: x) (addInAllLocations a ls') end.
imports: FCF.FCF FCF.CompFold FCF.RndListElem Permutation