proposition: Theorem getAllPermutations_not_nil : forall (A : Type)(ls : list A), getAllPermutations ls = nil -> False.
proof: Proof. induction ls; intuition; simpl in *. inversion H. case_eq (getAllPermutations ls); intuition. rewrite H0 in H. simpl in *. apply app_eq_nil in H. intuition. eapply addInAllLocations_not_nil; eauto. Qed.
imports: FCF.FCF FCF.CompFold FCF.RndListElem Permutation