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?
... and sometimes (induction a rule: function.induct ) is needed
Last updated: Sep 25 2021 at 09:17 UTC