proposition: Theorem TrueRepeat_G3_eq_sum : Pr[x <-$ TrueRepeat_G3; ret (fst x || snd x)] <= Pr[TrueMult_G _ c A1 f n] + expRat failProb n.
proof: Proof. rewrite evalDist_orb_le. rewrite G3_TrueMult_equiv. rewrite TrueRepeat_G1_bad_equiv . rewrite TrueRepeat_G2_bad_small. intuition. Qed.
imports: FCF.FCF FCF.CompFold FCF.RndNat FCF.Hybrid