proposition: Theorem evalDist_Repeat_0 : forall (A : Set)(c : Comp A)(P : A -> bool) a, (forall x, In x (getSupport c) -> P x = true -> x <> a) -> evalDist (Repeat c P) a == 0.
proof: Proof. intuition. simpl. unfold indicator. case_eq (P a); intuition. rewrite ratMult_1_l. eapply ratMult_0. right. eapply getSupport_not_In_evalDist. intuition. eapply H; eauto. rewrite ratMult_0_l. eapply ratMult_0_l. Qed.
imports: FCF.Crypto FCF.Bernoulli FCF.NotationV1