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