proposition: Theorem G1_eq_G1_count : Pr[G1] == Pr[x <-$ G1_count; ret (fst x)].
proof: Proof. unfold G1, G1_count. fcf_inline_first. fcf_to_prhl_eq. fcf_skip. fcf_inline_first. fcf_skip. eapply (fcf_oracle_eq (fun x y => x = fst y)); trivial; intuition; subst. unfold O1_count. fcf_simp. fcf_ident_expand_l. fcf_skip. fcf_spec_ret; intuition. simpl in *; intuition; subst. fcf_simp. simpl. eapply comp_spec_eq_refl. Qed.
imports: FCF.FCF FCF.RndInList