functor
  (S : Res.S) (A : sig
                     type hyp = S.St.formula list
                     val prove_hyp :
                       Format.formatter -> string -> hyp -> unit
                     val prove_lemma :
                       Format.formatter -> string -> S.lemma -> unit
                     val prove_assumption :
                       Format.formatter -> string -> S.St.formula -> unit
                   end) ->
  sig val print : Format.formatter -> S.proof -> unit end