p must have type K t₁ ... t_n = K' t'₁ ... t'_m where K and K' must be different constructors of the same inductive type and each argument list can be empty if its constructor takes no arguments.

It closes the current sequent by proving the absurdity of p.

None.