Proof-irrelevance out of excluded-middle and choice in the calculus of constructions
Franco Barbanera, Stefano Berardi · Journal of Functional Programming · 1996
Abstract We present a short and direct syntactic proof of the fact that adding the axiom of choice and the principle of excluded-middle to Coquand–Huet's Calculus of Constructions gives proof-irrelevance.