¹ is now a symbol

Fix in response to the fix to https://coq.inria.fr/bugs/show_bug.cgi?id=3541
More replacement of [projT] with [pr]

The instances of [proj1_sig] in Category/Sigma are intentional and
semantically meaningful (they are about subsets/sigT with an hProp).