module Clause_intf: sig .. end
sig
end
type proof_step = ProofStep.t
ProofStep.t
type proof = ProofStep.of_
ProofStep.of_
module type S = sig .. end