destruct [(id…)] [skip (id…)]

Each hypothesis H_i must be either a Leibniz or a John Major equality where the two sides of the equality are possibly applied constructors of an inductive type.

The tactic recursively compare the two sides of each equality looking for different constructors in corresponding position. If two of them are found, the tactic closes the current sequent by proving the absurdity of p. Otherwise it adds a new hypothesis for each leaf of the formula that states the equality of the subformulae in the corresponding positions on the two sides of the equality. If the newly added hypothesis is an equality between a variable and a term, the variable is substituted for the term everywhere in the sequent, except for the hypotheses K_j, and it is then cleared from the list of hypotheses.

None.