The intropattern {H} also meant clear (both in ssreflect, and the logic
part of the introduction pattern).

This class whose name is horrible and purpose is arbitrary seems to be a
leftover of some experiment with ch2o, a long time a ago.

That way type class search becomes more predictable.

Lifting lemmas : make the initial state appear under an existential under the view shift. This is still sound, but slightly more expressive.