proposition: Theorem IND_CPA_SecretKey_OI_G1_Hybrid : Pr[IND_CPA_SecretKey_OI_G1] == Pr[ListHybrid_G _ A1 A3 (fun x => key <-$ KeyGen; [b, _] <-$2 (A2 x) _ _ (EncryptNothingOracle _ ptDefault key) tt; ret b )].
proof: Proof. reflexivity. Qed.
imports: FCF.FCF FCF.CompFold FCF.Hybrid