Expose generalize tactic to the user

[jonsterling]

The “generalize” tactic is useful. We should expose it to the user!

[favonia]

What does it do?

[jonsterling]

@favonia If you are in a goal like !- P x, it changes the goal to !- (x : A) -> P x. This is used internally in the pattern inversion tactics, for instance.

Later when we add equality types, another version of the tactic that will be useful is one that turns the goal to !- (y : A) (p : x = y) -> P y. This will be essential for when we add indexed inductive types in the future.