A proof term that `S` and `T` are the same type (type identity). This type is only ever inhabited when S is nominally equivalent to T. ## A note on v