proposition: Theorem PRF_DRBG_G3_2_3_eq_until_bad : forall a : bool, evalDist PRF_DRBG_G3_2 (a, false) == evalDist PRF_DRBG_G3_3 (a, false).
proof: Proof. intuition. unfold PRF_DRBG_G3_2, PRF_DRBG_G3_3. fcf_to_prhl. fcf_skip. apply PRF_A_randomFunc_eq_until_bad. fcf_simp. fcf_spec_ret. simpl in *; pairInv; intuition; subst; trivial. simpl in *. pairInv. rewrite H2. rewrite <- H2 in H6. edestruct H3; intuition; subst. trivial. Qed.
imports: FCF HasDups RndInList CompFold Permutation PRF