proposition: Theorem addInAllLocations_not_nil : forall (A : Type) l (a : A), addInAllLocations a l = nil -> False.
proof: Proof. induction l; intuition; unfold addInAllLocations in *; simpl in *. inversion H. inversion H. Qed.
imports: FCF.FCF FCF.CompFold FCF.RndListElem Permutation