proposition: Theorem expected_poly_time_rnd_ident : efficient _ (fun n => ({0, 1} ^ n)).
proof: Proof. eapply expected_poly_time_rnd. exists 1%nat. exists 1%nat. exists 0%nat. intuition. simpl. lia. Qed.
imports: FCF.Crypto FCF.Asymptotic FCF.FCF