proposition: Theorem PRFE_Encrypt_wf : forall n x (y : Bvector n), well_formed_oc (PRFE_Encrypt_OC x y).
proof: Proof. intuition. econstructor. econstructor. wftac. intuition. econstructor. econstructor. intuition. econstructor. wftac. Qed.
imports: FCF PRF Encryption RndInList OTP WC_PolyTime Asymptotic