proposition: Theorem expected_poly_time_compose_0_binary : forall (A B C : nat -> Type)(f1 : forall n, A n)(f2 : forall n, B n)(f3 : forall n, A n -> B n -> C n) , efficient _ f1 -> efficient _ f2 -> efficient _ f3 -> efficient _ (fun n => f3 n (f1 n) (f2 n)).
proof: Proof. intuition. eapply (@expected_poly_time_compose_0 _ _ _ _ _ (fun n b => f3 n (f1 n) b)); eauto. eapply (@expected_poly_time_compose_0 _ _ _ _ _ (fun n b => f3 n b)); eauto. Qed.
imports: FCF.Crypto FCF.Asymptotic FCF.FCF