Why is the combination of
impredicativity + excluded middle + large elimination
inconsistent in dependent type theory?
My understanding of large elimination is I am doing large elimination if I am eliminating an inductive type to build a type.
I am trying to learn more about large elimination and how large elimination interacts with other constructs like predicativity and EM. In particular, I would like to know whether such inconsistency can be derived in for example, the impredicative Prop in Coq when large elimination is allowed and if so, how it's derived.