include "nat/count.ma".(*necessary just to use bool_to_nat and bool_to_nat_andb*)
(* sigma_p on nautral numbers is a specialization of sigma_p_gen *)
definition sigma_p: nat \to (nat \to bool) \to (nat \to nat) \to nat \def
include "nat/count.ma".(*necessary just to use bool_to_nat and bool_to_nat_andb*)
(* sigma_p on nautral numbers is a specialization of sigma_p_gen *)
definition sigma_p: nat \to (nat \to bool) \to (nat \to nat) \to nat \def