In the the standard library of Coq, there is the axiom:
Axiom JMeq_eq : forall (A:Type) (x y:A), JMeq x y -> x = y.
Why isn't it provable? Can it be reduced to more elementary axioms? Is it consistent with impredicative Set? Is there the same axiom in Agda?