https://softwarefoundations.cis.upenn.edu/draft/lf-current/Tactics.html#lab139
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.
When you 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 false.
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.