proposition: Theorem getAllPermutations_perms : forall (A : Set)(ls1 ls2 : list A), In ls2 (getAllPermutations ls1) -> Permutation ls1 ls2.
proof: Proof. induction ls1; intuition; simpl in *. intuition. subst. econstructor. eapply in_flatten in H. destruct H. intuition. eapply in_map_iff in H0. destruct H0. intuition. subst. eapply addInAllLocations_perm in H1. eapply perm_trans. 2:{ eapply Permutation_sym. eauto. } eapply perm_skip. eapply IHls1. trivial. Qed.
imports: FCF.FCF FCF.CompFold FCF.RndListElem Permutation