sig
  type formula
  type proof
  type level
  val dummy : Theory_intf.S.level
  val current_level : unit -> Theory_intf.S.level
  val assume :
    (Theory_intf.S.formula, Theory_intf.S.proof) Theory_intf.slice ->
    (Theory_intf.S.formula, Theory_intf.S.proof) Theory_intf.res
  val if_sat :
    (Theory_intf.S.formula, Theory_intf.S.proof) Theory_intf.slice ->
    (Theory_intf.S.formula, Theory_intf.S.proof) Theory_intf.res
  val backtrack : Theory_intf.S.level -> unit
end