proposition: Theorem rndBool_bind : forall (f : bool -> Comp bool), Pr[b <-$ {0, 1}; f b] == (1 / 2) * Pr[f true] + (1 / 2) * Pr[f false].
proof: Proof. intuition. simpl. destruct (bind_eq_dec ({ 0 , 1 }^1) (fun m : Bvector 1 => ret Vector.hd m) false true). discriminate. unfold sumList. simpl. destruct (EqDec_dec bool_EqDec true false). discriminate. destruct (EqDec_dec bool_EqDec false true). discriminate. destruct (EqDec_dec bool_EqDec true true). destruct (EqDec_dec bool_EqDec false false). repeat rewrite <- ratAdd_0_l. repeat rewrite ratMult_0_r. repeat rewrite <- ratAdd_0_r. repeat rewrite <- ratAdd_0_l. repeat rewrite ratMult_1_r. eapply ratAdd_eqRat_compat; eapply ratMult_eqRat_compat; intuition. intuition. intuition. Qed.
imports: FCF.FCF FCF.Crypto FCF.Asymptotic