generalize patt as H


generalize pattern [as id]


All the terms matched by patt must be convertible and close in the context of the current sequent.


It closes the current sequent by applying a stronger lemma that is proved using the new generated sequent.

New sequents to prove:

It opens a new sequent where the current sequent conclusion G is generalized to ∀x.G{x/t} where {x/t} is a notation for the replacement with x of all the occurrences of the term t matched by patt. If patt matches no subterm then t is defined as the wanted part of the pattern.