proposition: Theorem shuffle_Permutation : forall (ls1 ls2 : list A), In ls2 (getSupport (shuffle ls1)) -> Permutation ls1 ls2.
proof: Proof. intuition. unfold shuffle in *. repeat simp_in_support. destruct x. eapply rndListElem_support in H0. eapply getAllPermutations_perms. trivial. eapply rndListElem_support_None in H0. exfalso. eapply getAllPermutations_not_nil. eauto. Qed.
imports: FCF.FCF FCF.CompFold FCF.RndListElem Permutation