proposition: Theorem prob_fold_and_eq_exp_h : forall (A B : Set)(c : Comp A)(ls : list B)(P : A -> bool), Pr[compFold _ (fun b _ => x <-$ c; ret b && (P x)) true ls] == expRat (Pr[x <-$c; ret (P x)]) (length ls).
proof: Proof. induction ls; intuition. simpl. rewrite evalDist_ret_1; intuition. simpl. rewrite evalDist_seq_step. rewrite sumList_support_bool'. rewrite prob_fold_add_false_0. repeat rewrite ratMult_0_r. rewrite <- ratAdd_0_r. eapply ratMult_eqRat_compat; intuition. Qed.
imports: FCF.FCF Permutation