proposition: Theorem Def_equiv_2W : | Pr[StandardDef_G] - 1 / 2 | == (1 / 2) * | Pr[f eta false] - Pr[f eta true] |.
proof: Proof. rewrite StandardDef_equiv_2W_h. rewrite ratDistance_comm. intuition. Qed.
imports: FCF.FCF FCF.Crypto FCF.Asymptotic