proposition: Theorem OWP_HCP_PRG : PRG_Advantage OWP_HCP_PRG_fun A <= (HCP_Advantage f b B).
proof: Proof. unfold OWP_HCP_PRG_fun, PRG_Advantage, PRG_G1, PRG_G2, HCP_Advantage, HCP_G1, HCP_G2, B. eapply eqRat_impl_leRat. eapply ratDistance_eqRat_compat. intuition. eapply eqRat_trans. eapply evalDist_seq_eq. eapply rnd_concat_eq. intuition. eapply eqRat_refl. dist_inline_first. comp_skip. comp_simp. inline_first. eapply (distro_iso_eq f f_inv); intuition. simpl; eauto using in_getAllBvectors. apply uniformity. comp_simp. intuition. Qed.
imports: FCF.FCF FCF.SemEquiv