Gergely Buday (Jan 27 2021 at 11:21): Gergely Buday (Jan 27 2021 at 11:21):Suppose you have a goal of the form P(a) + P(b) = P(a+b) or something similar.
Sometimes (induction a) auto ...
sometimes (induction a b) auto ...
even other times (induction a arbitrary: b) auto ... works
Is there a rule, not necessarily formal, that tells us which one should I use?
Gergely Buday (Jan 27 2021 at 11:22):... and sometimes (induction a rule: function.induct ) is needed
Last updated: Apr 18 2024 at 20:16 UTC