proposition: Theorem RF_Encrypt_bad_wf : forall x a b, well_formed_comp (RF_Encrypt_bad x a b).
proof: Proof. intuition. unfold RF_Encrypt_bad; wftac. eapply randomFunc_wf; wftac. Qed.
imports: FCF PRF Encryption RndInList OTP WC_PolyTime