proposition: Theorem TrueMult_impl_Repeat : Pr[TrueRepeat_G] <= Pr[TrueMult_G _ c A1 f n] + (expRat failProb n).
proof: Proof. rewrite TrueRepeat_G_G1_equiv. rewrite TrueRepeat_G1_G2_equiv. rewrite TrueRepeat_G2_G3_equiv. eapply TrueRepeat_G3_eq_sum. Qed.
imports: FCF.FCF FCF.CompFold FCF.RndNat FCF.Hybrid