Work around bug 3539

This is https://coq.inria.fr/bugs/show_bug.cgi?id=3539, Unable to unify
"?25 (@pair ?23 ?24 (fst ?27) (snd ?27))" with "?25 ?27" on rewrite
Make [prod] a primitive record

This gives us judgmental eta for products.  Although there are still a
number of bugs in primitive projections and eta in general, there are
relatively few that are hit when we make just [prod] primitive.
Take advantage of judgmental eta to clean up