generalize pattern

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.

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.