clearbody id

H must be an hypothesis of the current sequent to prove.

It hides the definiens of a definition in the current sequent context. Thus the definition becomes an hypothesis.

None.