proposition: Theorem DistSingle_G1_equiv : DistSingle_Adv c1 c2 B1 B2 == (| Pr[DistSingle_G1 c1] - Pr[DistSingle_G1 c2] |).
proof: Proof. unfold DistSingle_Adv, DistSingle_G1, DistSingle_G. intuition. Qed.
imports: FCF.FCF FCF.CompFold FCF.RndNat FCF.Hybrid