[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?

I was learning Coq, but then I realized it sounds like cock and would put me in awkward situations. What were they thinking with that name...?

My other option now is Isabelle, but I know nothing about it.