proposition: Theorem G1_eq_Gi_q : Pr[G1] == Pr[Gi q].
proof: Proof. rewrite G1_eq_G1_count . rewrite Gi_eq_Gi_count. eapply ratIdentityIndiscernables. eapply leRat_impl_eqRat. eapply leRat_trans. eapply fundamental_lemma_h. unfold G1_count, Gi_count. fcf_inline_first. fcf_skip. fcf_simp. fcf_inline_first. fcf_to_prhl. comp_skip. apply O1_count_Oi_eq_until_bad. simpl in H1. intuition; subst. fcf_simp. simpl in *. fcf_spec_ret; fcf_compute. intuition. unfold G1_count, Gi_count. fcf_skip. fcf_simp. fcf_to_prhl. comp_skip. eapply O1_count_Oi_eq_until_bad. simpl in *; intuition. fcf_simp. destruct p; simpl in *. fcf_spec_ret; fcf_compute; assert (b1 <= q)%nat by lia; intuition; subst; pairInv; trivial. unfold G1_count. fcf_inline_first. fcf_irr_l. fcf_simp. inline_first. fcf_irr_l. apply oc_comp_wf; intuition. eapply O1_count_wf. fcf_simp. unfold snd. fcf_compute. destruct p. eapply (qam_count (A1_qam s s0 _) (fun x => snd x)) in H0. simpl in *. lia. intuition. simpl. apply O1_count_increases in H1. lia. trivial. eapply rat0_le_all. Unshelve. eauto. Qed.
imports: FCF.FCF FCF.RndInList