I'm playing around with Coq and Software Foundations and is somehow very confused by something I took for granted since forever.To proveTheorem app_length_cons : forall (X:Type) (l1:list X) (x:X),                              length (l1 ++ x :: l1) = S (length (l1 ++ l1)).we can first proveTheorem 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 -> IHl1'.  reflexivity.Qed.Then simplyProof.  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 proveTheorem app_length_cons'' : forall (X:Type) (l1:list X) (x:X),                              length (l1 ++ x :: l1) = S (length (l1 ++ l1)).use the same methodProof.  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?
Substituting two different identifiers with the same identifier in Coq - why does this work?
logic;induction;coq