-
Robbert Krebbers authored
The intropattern {H} also meant clear (both in ssreflect, and the logic part of the introduction pattern).
086cc92c
The intropattern {H} also meant clear (both in ssreflect, and the logic part of the introduction pattern).