proposition: Theorem expected_poly_time_bind_f : forall (A : nat -> Type)(B C : nat -> Set) (b : forall n, A n -> Comp (B n)) (c : forall n, A n -> B n -> Comp (C n)), efficient _ b -> efficient _ c -> efficient _ (fun n a => (Bind (b n a) (c n a))).
proof: Proof. intuition. eapply (@expected_poly_time_compose_binary _ _ _ _ b c (fun n a b => Bind a b)); eauto. eapply expected_poly_time_bind. Qed.
imports: FCF.Crypto FCF.Asymptotic FCF.FCF