sig
  type t
  type id
  type location
  val tType : Ast_zf.Term.t
  val wildcard : Ast_zf.Term.t
  val prop : Ast_zf.Term.t
  val true_ : Ast_zf.Term.t
  val false_ : Ast_zf.Term.t
  val const : ?loc:Ast_zf.Term.location -> Ast_zf.Term.id -> Ast_zf.Term.t
  val apply :
    ?loc:Ast_zf.Term.location ->
    Ast_zf.Term.t -> Ast_zf.Term.t list -> Ast_zf.Term.t
  val colon :
    ?loc:Ast_zf.Term.location ->
    Ast_zf.Term.t -> Ast_zf.Term.t -> Ast_zf.Term.t
  val arrow :
    ?loc:Ast_zf.Term.location ->
    Ast_zf.Term.t -> Ast_zf.Term.t -> Ast_zf.Term.t
  val eq :
    ?loc:Ast_zf.Term.location ->
    Ast_zf.Term.t -> Ast_zf.Term.t -> Ast_zf.Term.t
  val not_ : ?loc:Ast_zf.Term.location -> Ast_zf.Term.t -> Ast_zf.Term.t
  val or_ : ?loc:Ast_zf.Term.location -> Ast_zf.Term.t list -> Ast_zf.Term.t
  val and_ : ?loc:Ast_zf.Term.location -> Ast_zf.Term.t list -> Ast_zf.Term.t
  val imply :
    ?loc:Ast_zf.Term.location ->
    Ast_zf.Term.t -> Ast_zf.Term.t -> Ast_zf.Term.t
  val equiv :
    ?loc:Ast_zf.Term.location ->
    Ast_zf.Term.t -> Ast_zf.Term.t -> Ast_zf.Term.t
  val pi :
    ?loc:Ast_zf.Term.location ->
    Ast_zf.Term.t list -> Ast_zf.Term.t -> Ast_zf.Term.t
  val letin :
    ?loc:Ast_zf.Term.location ->
    Ast_zf.Term.t list -> Ast_zf.Term.t -> Ast_zf.Term.t
  val forall :
    ?loc:Ast_zf.Term.location ->
    Ast_zf.Term.t list -> Ast_zf.Term.t -> Ast_zf.Term.t
  val exists :
    ?loc:Ast_zf.Term.location ->
    Ast_zf.Term.t list -> Ast_zf.Term.t -> Ast_zf.Term.t
end