proposition: Theorem G2_3_4_bad_eq : Pr[x <-$ G2_3; ret (snd x)] == Pr[x <-$ G2_4; ret (snd x)].
proof: Proof. unfold G2_3, G2_4. inline_first. comp_skip. inline_first. eapply comp_spec_eq_impl_eq. comp_skip. eapply A_randomFunc_F_spec. simpl in *. comp_simp. simpl. eapply comp_spec_ret; intuition. Qed.
imports: FCF PRF SplitVector cAU CompFold DetSem SemEquiv