proposition: Theorem expected_poly_time_fst_f : forall (A B C : nat -> Type)(f : forall n, A n -> (B n * C n)), efficient _ f -> efficient _ (fun n (a : A n) => fst (f n a)).
proof: Proof. intuition. eapply (@expected_poly_time_compose_simp _ _ _ _ (fun n a => fst a)); eauto. eapply expected_poly_time_fst. Qed.
imports: FCF.Crypto FCF.Asymptotic FCF.FCF