clear H1 ... Hm
clear id [id…]
H1 ... Hm must be hypotheses of the current sequent to prove.
It hides the hypotheses H1 ... Hm from the current sequent.
None
Matita Home