sig
  type t = TypedSTerm.term
  type view =
      True
    | False
    | Atom of TypedSTerm.Form.t
    | Eq of TypedSTerm.Form.t * TypedSTerm.Form.t
    | Neq of TypedSTerm.Form.t * TypedSTerm.Form.t
    | Equiv of TypedSTerm.Form.t * TypedSTerm.Form.t
    | Xor of TypedSTerm.Form.t * TypedSTerm.Form.t
    | Imply of TypedSTerm.Form.t * TypedSTerm.Form.t
    | And of TypedSTerm.Form.t list
    | Or of TypedSTerm.Form.t list
    | Not of TypedSTerm.Form.t
    | Forall of TypedSTerm.Form.t Var.t * TypedSTerm.Form.t
    | Exists of TypedSTerm.Form.t Var.t * TypedSTerm.Form.t
  val view : TypedSTerm.Form.t -> TypedSTerm.Form.view
  val true_ : TypedSTerm.Form.t
  val false_ : TypedSTerm.Form.t
  val atom : TypedSTerm.Form.t -> TypedSTerm.Form.t
  val eq :
    ?loc:TypedSTerm.location ->
    TypedSTerm.Form.t -> TypedSTerm.Form.t -> TypedSTerm.Form.t
  val neq :
    ?loc:TypedSTerm.location ->
    TypedSTerm.Form.t -> TypedSTerm.Form.t -> TypedSTerm.Form.t
  val equiv :
    ?loc:TypedSTerm.location ->
    TypedSTerm.Form.t -> TypedSTerm.Form.t -> TypedSTerm.Form.t
  val xor :
    ?loc:TypedSTerm.location ->
    TypedSTerm.Form.t -> TypedSTerm.Form.t -> TypedSTerm.Form.t
  val imply :
    ?loc:TypedSTerm.location ->
    TypedSTerm.Form.t -> TypedSTerm.Form.t -> TypedSTerm.Form.t
  val and_ :
    ?loc:TypedSTerm.location -> TypedSTerm.Form.t list -> TypedSTerm.Form.t
  val or_ :
    ?loc:TypedSTerm.location -> TypedSTerm.Form.t list -> TypedSTerm.Form.t
  val not_ :
    ?loc:TypedSTerm.location -> TypedSTerm.Form.t -> TypedSTerm.Form.t
  val forall :
    ?loc:TypedSTerm.location ->
    TypedSTerm.Form.t Var.t -> TypedSTerm.Form.t -> TypedSTerm.Form.t
  val exists :
    ?loc:TypedSTerm.location ->
    TypedSTerm.Form.t Var.t -> TypedSTerm.Form.t -> TypedSTerm.Form.t
  val forall_l :
    ?loc:TypedSTerm.location ->
    TypedSTerm.Form.t Var.t list -> TypedSTerm.Form.t -> TypedSTerm.Form.t
  val exists_l :
    ?loc:TypedSTerm.location ->
    TypedSTerm.Form.t Var.t list -> TypedSTerm.Form.t -> TypedSTerm.Form.t
  val close_forall :
    ?loc:TypedSTerm.location -> TypedSTerm.Form.t -> TypedSTerm.Form.t
end