Coq : transitivity fails on list intermediate term

Question

I'm doing this exercises from LF:

Example injection_ex3 : ∀ (X : Type) (x y z : X) (l j : list X),
  x :: y :: l = z :: j →
  j = z :: l →
  x = y.

My question is that why transitivity fails here:

Proof.
  intros X x y z l j H I. 
  injection H as J.
  Fail transitivity j. (* shouldn't fail imho *) 

The environment at this point:

1 subgoal

X : Type
x, y, z : X
l, j : list X
J : x = z
H : y :: l = j
I : j = z :: l

========================= (1 / 1)

x = y

And the error is :

The command has indeed failed with message:
In environment
X : Type
x, y, z : X
l, j : list X
J : x = z
H : y :: l = j
I : j = z :: l
The term "j" has type "list X" while it is expected to have type "X".  

It seems quite straightforward here that j is the intermediate term and it should be "list X".
What was wrong?