proposition: Theorem shuffle_RndPerm_spec : forall (A : Set)(eqd : EqDec A)(ls : list A), comp_spec (fun a b => a = permute ls b) (shuffle eqd ls) (shuffle _ (allNatsLt (length ls))).
proof: Proof. intuition. unfold shuffle in *. comp_skip. eapply rndListElem_pred. eapply getAllPerms_permute_eq. simpl in H1. eapply comp_spec_ret; intuition. destruct a. destruct H1. intuition. subst. trivial. subst. simpl. intuition. Qed.
imports: FCF.FCF FCF.CompFold FCF.RndListElem Permutation