sig
  type hyp
  type lemma
  type assumption
  val prove_hyp : Format.formatter -> string -> Coq.Arg.hyp -> unit
  val prove_lemma : Format.formatter -> string -> Coq.Arg.lemma -> unit
  val prove_assumption :
    Format.formatter -> string -> Coq.Arg.assumption -> unit
end