clean up

1. Fix some confusion about "pr1" versus "pr1weq".

2. Make isweqtoforallpaths opaque with "Qed", fixing a problem
   in toforallpaths_funextsec.

3. Change the definition of total2 to a "primitive" record, to
   prepare for forthcoming "primitive" projections.