functor
  (S : Res.S) (A : sig
                     val print_atom : Format.formatter -> S.atom -> unit
                     val lemma_info :
                       S.lemma ->
                       string * string option *
                       (Format.formatter -> unit -> unit) list
                   end) ->
  sig val print : Format.formatter -> S.proof -> unit end