proposition: Theorem Gi_oracleMap'_equiv : forall i, Pr[Gi_oracleMap i] == Pr[Gi_oracleMap' i].
proof: Proof. intuition. unfold Gi_oracleMap, Gi_oracleMap'. fcf_skip. fcf_simp. fcf_skip. replace l with (firstn i l ++ skipn i l). eapply eqRat_trans. eapply compFold_app. fcf_skip. rewrite firstn_skipn. reflexivity. fcf_simp. fcf_ident_expand_l. fcf_to_prhl_eq. rewrite firstn_skipn. fcf_skip. eapply (compFold_spec' (fun a b c d => a = b /\ snd c = snd d /\ l0++ (fst d) = (fst c))); intuition idtac. simpl. eapply app_nil_r. simpl in *. subst. destruct d. simpl in *. subst. unfold Oi. inversion H2; clear H2; subst. fcf_inline_first. fcf_skip. fcf_simp. fcf_spec_ret. simpl. rewrite app_assoc. trivial. fcf_simp. simpl in H3. intuition. subst. fcf_spec_ret. rewrite firstn_skipn. trivial. Qed.
imports: FCF.FCF FCF.RndInList FCF.CompFold FCF.OracleCompFold FCF.PRF