proposition: Theorem RPS_G0_equiv : Pr[RPS_G0] == Pr[x <-$ RPS_G_1; ret fst x].
proof: Proof. unfold RPS_G0, RPS_G_1. inline_first. eapply (comp_spec_eq_impl_eq). comp_skip. eapply (@oc_comp_spec_eq _ _ _ _ _ _ _ _ _ _ _ _ _ _ (fun a b => a = fst b)); trivial. intuition. subst. unfold randomFunc, randomFunc_bad. comp_simp. simpl. case_eq ( arrayLookup eqdd l a ); intuition. eapply comp_spec_ret; intuition. comp_skip. eapply comp_base_exists; eauto. eapply comp_base_exists; eauto. eapply comp_spec_ret; intuition. comp_simp. simpl in *; intuition. subst. eapply comp_spec_eq_refl. Qed.
imports: FCF PRF RndInList