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