proposition: Theorem expected_poly_time_ret_f : forall (A : nat -> Type)(B : nat -> Set)(eqd : forall n, eq_dec (B n))(f : forall n, (A n) -> (B n)), efficient _ f -> efficient _ (fun n (a : A n) => Ret (eqd n) (f n a)).
proof: Proof. intuition. eapply (@expected_poly_time_compose_simp _ _ _ _ (fun n b => Ret (eqd n) b)); eauto. eapply expected_poly_time_ret. Qed.
imports: FCF.Crypto FCF.Asymptotic FCF.FCF