Post #4230139

I just learned that the strong J (the SProp-to-Type elimination for the strict identity type) is actually okay and it is discussed already in the paper on definitional proof-irrelevance. I should have read the paper more carefully..