sig
  module type S = Backend_intf.S
  module type Arg =
    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
  module Make :
    functor
      (S : Res.S) (A : sig
                         val print : Format.formatter -> S.St.formula -> unit
                         val prove : Format.formatter -> S.lemma -> unit
                         val context : Format.formatter -> S.proof -> unit
                       end) ->
      sig val print : Format.formatter -> S.proof -> unit end
end