Designing a space-efficient cast representation that is good for both mechanized metatheory and implementation is challenging. Existing solutions (i.e. coercions, threesomes, and supercoercions) are good for one or the other. This paper presents a new cast representation, named hypercoercions, that is good for both. On the way to proving the correctness of hypercoercions, this paper also makes progress on a general framework for proving the correctness of cast representations.