contradiction

There must be in the current context an hypothesis of type False.

It closes the current sequent by applying an hypothesis of type False.

None