fact: Definition B2(s : A * A_State)(b : B) : Comp bool := [a, s_A] <-2 s; i <-$ [0 .. n); rndHybrid <-$ computeHybrid n i a; distHybrid <- listReplace rndHybrid i b b; A2 s_A distHybrid.
imports: FCF.FCF FCF.CompFold FCF.RndNat FCF.Hybrid