We describe an approach for combining theorem proving techniques with static analysis to analyze data structure consistency for programs that manipulate heterogeneous data structures. Our system uses interactive theorem proving and shape analysis to verify that data structure implementations conform to set interfaces. A simpler static analysis uses the verified set interfaces to verify properties that characterize how shared objects participate in multiple data structures. We have successfully applied this technique to several programs and found that we were able to effectively use theorem proving within circumscribed regions of the program to enable the verification, with an appropriate amount of effort, of large-scale program properties.