I'm doing `generalize dependent a. generalize dependent b`

is there anything like `generalize dependent a, b`

?

There's `revert a b`

although you have to also mention the hypotheses that depend on those variables, and otherwise you can define your own tactic `Ltac gd2 a b := generalize dependent a; generalize dependent b.`

Hmm a custom tactic is a good idea, thank you!

Last updated: Jun 24 2024 at 01:01 UTC