The Coq mailing list

[Jonathan <jonikelee AT gmail.com>]

On 10/07/2014 01:44 PM, Eddy Westbrook wrote:
> Jonathon,
>
> Echoing what Arnaud says here, I think this is one of those cases where an 
> axiom that seems innocuous in fact is not: even though it seems like this 
> sort of elimination would not be that big of an extension to Coq, in fact it 
> is.
>
> Another way to think about it: if you allowed Prop elimination to predicative 
> types, even just in a Prop-rooted subtree, those predicative types would 
> still have to contain a lot more elements, to accommodate Prop-elimination, 
> and this would significantly change the logic.
>
> -Eddy

Yes - put this in the category of wishful thinking.

-- Jonathan