proposition: Theorem shuffle_RndPerm_spec_eq : forall (A : Set)(eqd : EqDec A)(ls : list A), comp_spec eq (shuffle eqd ls) (x <-$ RndPerm (length ls); ret permute ls x).
proof: Proof. intuition. eapply comp_spec_eq_trans. eapply comp_spec_eq_symm. eapply comp_spec_right_ident. comp_skip. eapply shuffle_RndPerm_spec. eapply comp_spec_ret; intuition. Qed.
imports: FCF.FCF FCF.CompFold FCF.RndListElem Permutation