By introducing a variable you are saying for a “particular” instance of that variable. Not for all such instances of the variable.
Thus, when introducing more than necessary prior to induction you may unintentionally weaken the induction hypothesis that you will get, making it impossible to prove your goal.
destruct a compound expression you lose what the original equation was. For instance:
destruct (beq_nat 3 n).
will give you two subgoals. One where
(beq_nat 3 n) is replaced with
true, and one where it is replaced with
Sometimes, however, you actually need the fact that
(beq_nat 3 n)
= true in that branch of the proof, or that
(beq_nat 3 n) =
false in the other branch of the proof. You can keep this information with:
destruct (beq_nat 3 n) eqn:Hbeq3.
Which will introduce in the context a hypothesis
Hbeq3 which will be
beq_nat 3 n = true in the
true branch of the proof, and
beq_nat 3 n = false in the false branch.