[coq] sigma inversion

Hey, how can I prove:

X : Set
Y : X -> Set
x: X
y, z: Y x
H: existT _ x y = existT _ x z
========================
y = z

why does inversion not give me y=z? Is there some reason why it is not true?

>>6
i think you can find example of this in the standard library