proposition: Theorem prob_fold_add_false_0 : forall (A : Set)(B : Type)(c : Comp A)(ls : list B)(P : A -> bool), Pr[compFold _ (fun b _ => x <-$ c; ret b && (P x)) false ls] == 0.
proof: Proof. induction ls; intuition. simpl. rewrite evalDist_ret_0; intuition. simpl. inline_first. eapply leRat_impl_eqRat. eapply distro_irr_le. intuition. comp_simp. rewrite IHls. intuition. eapply rat0_le_all. Qed.
imports: FCF.FCF Permutation