refactor(tactic/generalizes): reimplement generalizes' (#3416)
The new implementation is somewhat simpler. It is inspired by the C++
function `generalize_indices` in `library/tactic/cases_tactic.cpp`,
which performs essentially the same construction.
The only non-internal change is the return type of `generalizes_intro`.
