`isValid` soundness hole?

We model `isValid` by providing a default implementation of `isValid _ := True` which can be overridden when an explicit definition is provided in a Hermes annotation.

However, I *suspect* this means that, given `T` with a non-trivial `isValid`, `(T, U)` will still have a trivial `isValid` since we don't explicitly provide an implementation for tuples which recurses into fields. Presumably the same hole exists with other compound types.