proposition: Theorem G2_eq_Gi_0 : Pr[G2] == Pr[Gi 0%nat].
proof: Proof. unfold G2, Gi. fcf_skip. fcf_simp. fcf_to_prhl_eq. comp_skip. eapply (fcf_oracle_eq (fun a b => a = fst b)); trivial; intuition; subst. unfold Oi. comp_simp. destruct (ge_dec n 0). simpl. fcf_ident_expand_l. comp_skip. eapply comp_spec_ret; intuition. lia. simpl in H1. intuition; subst. comp_simp. simpl in *. intuition; subst. eapply comp_spec_eq_refl. Qed.
imports: FCF.FCF FCF.RndInList