Matita Home

`generalize patt`

- Synopsis:
**generalize***pattern*- Pre-conditions:
All the terms matched by

**patt**must be convertible and close in the context of the current sequent.- Action:
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.