proposition: Theorem RndInList_prob : forall (ls : list (Bvector eta))(q : nat), length ls <= q -> (Pr[r <-$ {0, 1}^eta; ret (if (in_dec (EqDec_dec _) r ls) then true else false) ] <= q / 2 ^ eta)%rat.
proof: Proof. intuition. eapply leRat_trans. eapply RndInList_prob_h. eapply leRat_terms; intuition. Qed.
imports: FCF.FCF