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