sig
  type 'a t = 'a Syntax.formula
  val equal : 'a Syntax.formula -> 'a Syntax.formula -> bool
  val compare : 'a Syntax.formula -> 'a Syntax.formula -> int
  val hash : 'a Syntax.formula -> int
  val pp :
    ?env:string Syntax.Env.t ->
    'a Syntax.context -> Format.formatter -> 'a Syntax.formula -> unit
  val show :
    ?env:string Syntax.Env.t ->
    'a Syntax.context -> 'a Syntax.formula -> string
  val destruct :
    'a Syntax.context ->
    'a Syntax.formula -> ('a Syntax.formula, 'a) Syntax.open_formula
  val eval :
    'a Syntax.context ->
    (('b, 'a) Syntax.open_formula -> 'b) -> 'a Syntax.formula -> 'b
  val eval_memo :
    'a Syntax.context ->
    (('b, 'a) Syntax.open_formula -> 'b) -> 'a Syntax.formula -> 'b
  val existential_closure :
    'a Syntax.context -> 'a Syntax.formula -> 'a Syntax.formula
  val universal_closure :
    'a Syntax.context -> 'a Syntax.formula -> 'a Syntax.formula
  val skolemize_free :
    'a Syntax.context -> 'a Syntax.formula -> 'a Syntax.formula
  val prenex : 'a Syntax.context -> 'a Syntax.formula -> 'a Syntax.formula
end