proposition: Theorem G0_1_G0_equiv : Pr[G0_1] == Pr[G0].
proof: Proof. unfold G0_1, G0. eapply eqRat_trans. eapply evalDist_seq_eq. eapply Rnd_split_equiv. intros. eapply eqRat_refl. inline_first. comp_swap_r. comp_skip. inline_first. comp_skip. Qed.
imports: FCF PRF SplitVector cAU CompFold DetSem SemEquiv