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