tbrs2

Deducing propositional uniqueness for product types

1

In basics.tex, line 1372 (proof of 2.6.4 in the book), the proof concludes with ``` Thus, it remains to show $x = (\proj1 x, \proj2x)$. But this is the propositional...