proposition: Theorem RndInList_Prob : forall (a : list A), Pr[RndInList_G a] <= (length a)/1 * r.
proof: Proof. Local Opaque evalDist. unfold RndInList_G in *. induction a; intuition idtac; simpl in *. fcf_irr_l. rewrite evalDist_ret_0. eapply rat0_le_all. intuition idtac. discriminate. eapply leRat_trans. eapply (evalDist_bind_event_le _ _ (fun x => eqb a x || if (in_dec (EqDec_dec _) x a0) then true else false)). rewrite evalDist_orb_le. rewrite <- evalDist_event_equiv. rewrite IHa. rewrite collProb. reflexivity. intros. apply orb_false_elim in H0. intuition idtac. destruct (EqDec_dec eqda a a1). subst. rewrite eqb_refl in *. discriminate. destruct (in_dec (EqDec_dec eqda) a1 a0). discriminate. rewrite evalDist_ret_0. eapply rat0_le_all. intuition idtac. discriminate. rewrite <- ratAdd_0_r. rewrite ratMult_comm. rewrite ratMult_ratAdd_cd. simpl. rewrite ratMult_comm. reflexivity. Qed.
imports: FCF FCF.CompFold FCF.RndInList