fact: Definition G2_3_bad := k_in <-$ {0, 1}^k; [p, _] <-$2 au_F_A _ _ (WCR_Oracle _ F k_in) tt; [d1, d2] <-2 p; ret (negb (eqb d1 d2) && eqb (F k_in d1) (F k_in d2)).
imports: FCF PRF SplitVector cAU CompFold DetSem SemEquiv