proposition: Theorem G0_G1_1_equiv : Pr[G0] == Pr[G1_1].
proof: Proof. unfold G0, G1_1. comp_swap_l. comp_skip. unfold PRF_h_A. simpl. inline_first. comp_skip. comp_simp. inline_first. unfold f_oracle. eapply comp_spec_eq_impl_eq. comp_skip. eapply (@oc_comp_spec_eq _ _ _ _ _ _ _ _ _ _ _ _ _ _ (fun a b => True)). trivial. intuition. inline_first. comp_simp. inline_first. comp_simp. simpl. eapply comp_spec_ret; intuition. simpl in *. intuition; subst. comp_simp. simpl. inline_first. comp_simp. eapply comp_spec_eq_refl. Qed.
imports: FCF PRF SplitVector cAU CompFold DetSem SemEquiv