proposition: Theorem OMH_G_i_equiv : forall i, Pr[Gi_oracleMap' i] == Pr[OMH_G_i i].
proof: Proof. intuition. unfold Gi_oracleMap', OMH_G_i. fcf_skip. fcf_simp. fcf_inline_first. fcf_to_prhl_eq. fcf_skip. eapply (compFold_spec' (fun a b c d => a = b /\ fst c = fst d /\ fst (snd c) = snd d /\ (snd (snd c) + length a = min i (length l))%nat)); intuition. simpl. apply firstn_length. fcf_simp. simpl in *. subst. inversion H1; clear H1; subst. fcf_inline_first. destruct (ge_dec b2 i). exfalso. destruct (le_dec i (length l)). rewrite min_l in H4. lia. trivial. rewrite min_r in H4. lia. lia. comp_skip. fcf_spec_ret. simpl. lia. simpl in H2. intuition. subst. fcf_inline_first. fcf_simp. rewrite Nat.add_0_r in H6. destruct (ge_dec i (length l)). rewrite skipn_ge_nil; trivial. unfold oracleMap. simpl. fcf_simp. simpl. eapply comp_spec_eq_refl. fcf_skip. eapply (compFold_spec' (fun a b c d => a = b /\ fst c = fst d /\ fst (snd c) = snd d /\ (snd (snd c) >= i)%nat)); intuition. simpl. rewrite min_l; lia. simpl in *. subst. destruct (ge_dec b2 i); try lia. inversion H4; clear H4; subst. fcf_inline_first. fcf_simp. fcf_skip. simpl. fcf_spec_ret. simpl. lia. simpl in H5. intuition; subst. fcf_simp. simpl. eapply comp_spec_eq_refl. Qed.
imports: FCF.FCF FCF.RndInList FCF.CompFold FCF.OracleCompFold FCF.PRF