An interesting goal is for SMT solvers to produce independently checkable proofs. SMT languages already have expressive power that goes beyond first-order languages, and further extensions would give even more expressive power by allowing quantification over function types. Indeed, such extensions are considered in the current proposal for the new standard SMT3. Given the expressive power of SMT and its extensions, careful thought must be given to the intended semantics and an appropriate notion of proof. We propose higher-order set theory as an appropriate interpretation of SMT (and extensions) and obtain an adequate notion of SMT proofs via proof terms in higher-order set theory. To demonstrate the strength of this approach, we give a number of abstract examples that would be dificult to handle by other notions of proof. To demonstrate the practicality of the approach, we describe a family of integer diference logic examples. We give proof terms for each of these examples and check the correctness of the proofs using two proof checkers: the proof checker distributed with the Proofgold system and an alternative checker we have implemented that does not rely on access to the Proofgold block chain.