proposition: Theorem Gi_eq_Gi_count : forall i, Pr[Gi i] == Pr[x <-$ Gi_count i; ret (fst x)].
proof: Proof. intuition. unfold Gi_count, Gi. fcf_inline_first. fcf_skip. fcf_simp. fcf_inline_first. fcf_skip. fcf_simp. simpl. intuition. Qed.
imports: FCF.FCF FCF.RndInList