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

you cant because type theory is bullshit
you need an axiom called uniqueness of identity proofs
but the CIA nigger haskell gang decided to steer the entire type theory community down a wild goose chase of homotopy type theory, making their entire ethos about not being able to prove basic true equalities like this
rip coq, had so much potential before homos took over