Make `BiLaterContractive` a class instead of a notation.

This avoids unnecessary search on failed attempts. `Contractive` is notation for
`Proper`, so previously, this caused a bunch of setoid instances to be used. In
turn, this resulted in TC debug output that is hard to read.