Substituting two different identifiers with the same identifier in Coq - why does this work? I'm playing around with Coq and Software Foundations and is somehow very confused by something I took for granted since forever.

To prove

Theorem app_length_cons : forall (X:Type) (l1:list X) (x:X),
                              length (l1 ++ x :: l1) = S (length (l1 ++ l1)).


we can first prove

Theorem app_length_cons' : forall (X:Type) (l1 l2:list X) (x:X),
                             length (l1 ++ x :: l2) = S (length (l1 ++ l2)).


which is a straightforward induction,

Proof.
  intros.
  induction l1 as [| h l1'].
  reflexivity.
  simpl.
  rewrite -&gt; IHl1'.
  reflexivity.
Qed.


Then simply

Proof.
  intros.
  apply app_length_cons' with (l1:=l1) (l2:=l1).
Qed.


However, there is something strange going on here - in the induction proof, we are doing induction on l1 and not l2 - and from the proof, it looks like we are assuming l2 doesn't change in the induction case. But when we later apply it with l2:=l1, we are breaking this assumption.

Indeed, if we try to prove

Theorem app_length_cons'' : forall (X:Type) (l1:list X) (x:X),
                              length (l1 ++ x :: l1) = S (length (l1 ++ l1)).


use the same method

Proof.
  intros.
  induction l1 as [| h l1'].
  reflexivity.
  simpl.
  -- Can't rewrite use IHl1' : length (l1' ++ x :: l1') = S (length (l1' ++ l1')),
  -- since the goal is S (length (l1' ++ x :: h :: l1')) = S (S (length (l1' ++ h :: l1')))


it looks like the assumption that l2 doesn't change is broken thus the proof won't work.

I'm pretty sure I'm missing something here. Why can we substitute different identifiers with the same identifier?
it looks like we are assuming l2 doesn't change in the induction case.
  But when we later apply it with l2:=l1, we are breaking this
  assumption.


No. If we regard l1 to be a value which is repeatedly decreased in the induction proof, note that we let l2 to be equal to the initial value of l1 -- such value will not change in the induction steps. In other words: the value of l1 will decrease, but l2 will always be the initial value of l1.

We can even compare it with recursion in programming:

# pseudocode
def f(x, y):
   if x==0: return baseValue
   use f(x-1, y)
   return something


Just because f(x, y) is defined by induction on x, it does not mean that later on we can't call f(a, a) where both arguments have the same value a.