Why is the proof complete after proving only for one induction when we have more than one variable?

So I’m self-learning coq. And I came across the proof for associativity in addition forall (a b c : nat)

enter image description here

Appearntly when we do induction a. after intros a b c., it creates 2 subgoals

enter image description here

and afterwards we simply need to show that the two sides in both subgoals are equivalent, and the proof is completed.

So I’m just wondering why we don’t need to do induction b. and induction c. to complete the proof? Why only performing induction on a is able to complete the proof?

Or in other words, how come in the function that returns the proof, we just get b and c for “free”? Constructively don’t we need something like a double induction applied twice?

enter image description here