proposition: Theorem expected_poly_time_rndbool : efficient _ (fun (n : nat) => {0, 1}).
proof: Proof. eapply expected_poly_time_bind_0_f. eapply expected_poly_time_rnd. exists 0%nat. exists 1%nat. exists 0%nat. intuition. eapply expected_poly_time_ret_f. eapply expected_poly_time_vec_hd. Qed.
imports: FCF.Crypto FCF.Asymptotic FCF.FCF