proposition: Theorem PRF_A'_equiv : forall (S : Set)(eqds : EqDec S)(o : S -> (Bvector eta) -> Comp ((Bvector eta) * S)) s x, evalDist (PRF_A _ _ o s) x == evalDist (PRF_A' _ _ o s) x.
proof: Proof. intuition. unfold PRF_A, PRF_A'. do 5 (comp_simp; simpl; comp_skip; try eapply eqRat_refl). comp_simp; simpl. comp_simp. intuition. Qed.
imports: FCF PRF Encryption RndInList OTP WC_PolyTime