proposition: Theorem RF_Encrypt_bad_preserved : forall a c d e f g h, In (a, (c, d)) (getSupport (RF_Encrypt_bad e (f, g) h)) -> g = true -> d = true.
proof: Proof. intuition. unfold RF_Encrypt_bad in *. repeat simp_in_support. destruct x0. repeat simp_in_support. eapply orb_true_l. Qed.
imports: FCF PRF Encryption RndInList OTP WC_PolyTime