The inspect definition is used to pack a value with a proof
of an equality to itself. When pattern matching on the first component in
this existential type, we keep information about the origin of the pattern
available in the second component, the equality.