destruct

destruct p

Synopsis:

destruct sterm

Pre-conditions:

p must have type E1 = E2 where the two sides of the equality are possibly applied constructors of an inductive type.

Action:

The tactic recursively compare the two sides of the 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.

New sequents to prove:

None.