sig
  type 'a t
  val pp : Format.formatter -> 'a t -> unit
  val show : 'a t -> string
  val closure : 'a t -> 'a Syntax.formula
  val join : 'a t -> 'a t -> 'a t
  val widen : 'a t -> 'a t -> 'a t
  val equal : 'a t -> 'a t -> bool
  val tr_symbols : 'a t -> (Syntax.symbol * Syntax.symbol) list
  val abstract_iter :
    ?exists:(Syntax.symbol -> bool) ->
    'a Syntax.context ->
    'a Syntax.formula -> (Syntax.symbol * Syntax.symbol) list -> 'a t
  val closure_plus : 'a t -> 'a Syntax.formula
end