proposition: Theorem G1_2_G1_equiv : Pr[G1_2] == Pr[G1].
proof: Proof. unfold G1_2, G1. unfold PRF_h_A. simpl. inline_first. comp_skip. inline_first. eapply comp_spec_eq_impl_eq. comp_skip. eapply (@oc_comp_spec_eq _ _ _ _ _ _ _ _ _ _ _ _ _ _ (fun a b => snd a = b)). trivial. intuition. subst. inline_first. simpl. eapply comp_spec_eq_trans_r. 2:{ eapply comp_spec_right_ident. } comp_skip. apply (oneVector c). apply (oneVector c). inline_first. simpl. eapply comp_spec_ret; intuition. simpl in *. intuition; subst. inline_first. comp_simp. simpl. eapply comp_spec_eq_refl. Qed.
imports: FCF PRF SplitVector cAU CompFold DetSem SemEquiv