sig   type t   type id   type term   type location   val data :     ?loc:Ast_zf.Statement.location ->     Ast_zf.Statement.t list -> Ast_zf.Statement.t   val decl :     ?loc:Ast_zf.Statement.location ->     Ast_zf.Statement.id -> Ast_zf.Statement.term -> Ast_zf.Statement.t   val definition :     ?loc:Ast_zf.Statement.location ->     Ast_zf.Statement.id ->     Ast_zf.Statement.term -> Ast_zf.Statement.term -> Ast_zf.Statement.t   val inductive :     ?loc:Ast_zf.Statement.location ->     Ast_zf.Statement.id ->     Ast_zf.Statement.term list ->     (Ast_zf.Statement.id * Ast_zf.Statement.term list) list ->     Ast_zf.Statement.t   val rewrite :     ?loc:Ast_zf.Statement.location ->     ?attr:Ast_zf.Statement.term ->     Ast_zf.Statement.term -> Ast_zf.Statement.t   val goal :     ?loc:Ast_zf.Statement.location ->     ?attr:Ast_zf.Statement.term ->     Ast_zf.Statement.term -> Ast_zf.Statement.t   val assume :     ?loc:Ast_zf.Statement.location ->     ?attr:Ast_zf.Statement.term ->     Ast_zf.Statement.term -> Ast_zf.Statement.t end