proposition: Theorem RndPerm_In_support : forall n ls, In ls (getSupport (RndPerm n)) -> Permutation (allNatsLt n) ls.
proof: Proof. intuition. eapply shuffle_Permutation. eapply H. Qed.
imports: FCF.FCF FCF.CompFold FCF.RndListElem Permutation