sig
  type lemma
  type proof
  type formula
  val print : Format.formatter -> Dedukti.Arg.formula -> unit
  val prove : Format.formatter -> Dedukti.Arg.lemma -> unit
  val context : Format.formatter -> Dedukti.Arg.proof -> unit
end