let mk_unary_app ctx f x = Z3.mk_app ctx f [|x|]