sig
  type env
  type tau = Lang.F.tau
  type var = Lang.F.var
  type field = Lang.field
  type lfun = Lang.lfun
  type term = Lang.F.term
  type pred = Lang.F.pred
  val env : Lang.F.Vars.t -> Repr.env
  type repr =
      True
    | False
    | And of Repr.term list
    | Or of Repr.term list
    | Not of Repr.term
    | Imply of Repr.term list * Repr.term
    | If of Repr.term * Repr.term * Repr.term
    | Forall of Repr.tau * (Repr.env -> Repr.var * Repr.term)
    | Exists of Repr.tau * (Repr.env -> Repr.var * Repr.term)
    | Var of Repr.var
    | Int of Z.t
    | Real of Q.t
    | Add of Repr.term list
    | Mul of Repr.term list
    | Div of Repr.term * Repr.term
    | Mod of Repr.term * Repr.term
    | Eq of Repr.term * Repr.term
    | Neq of Repr.term * Repr.term
    | Lt of Repr.term * Repr.term
    | Leq of Repr.term * Repr.term
    | Times of Z.t * Repr.term
    | Call of Repr.lfun * Repr.term list
    | Field of Repr.term * Repr.field
    | Record of (Repr.field * Repr.term) list
    | Cst of Repr.tau * Repr.term
    | Get of Repr.term * Repr.term
    | Set of Repr.term * Repr.term * Repr.term
    | Abstract
  val term : Repr.term -> Repr.repr
  val pred : Repr.pred -> Repr.repr
  val lfun : Repr.lfun -> string
  val field : Repr.field -> string
end