Msat.EXPR
type proof
An abstract type for proofs
module Term : sig ... end
module Value : sig ... end
module Formula : Solver_intf.FORMULA