sig
  module Var :
    sig
      type t = int
      val fresh : unit -> Globular.Theory.Var.t
      val to_string : Globular.Theory.Var.t -> string
    end
  module Cons :
    sig
      type t = int
      val fresh : unit -> Globular.Theory.Cons.t
      val to_string : Globular.Theory.Cons.t -> string
    end
  type term =
      Var of Globular.Theory.Var.t
    | Cons of Globular.Theory.Cons.t * Globular.Theory.context
  and context =
      (Globular.Theory.term * (Globular.Theory.term * Globular.Theory.term))
      list
end