proposition: Theorem prob_fold_and_eq_exp : forall (A : Set)(c : Comp A)(n : nat)(P : A -> bool), Pr[compFold _ (fun b _ => x <-$ c; ret b && (P x)) true (forNats n)] == expRat (Pr[x <-$c; ret (P x)]) n.
proof: Proof. intuition. rewrite prob_fold_and_eq_exp_h. rewrite forNats_length. reflexivity. Qed.
imports: FCF.FCF Permutation