Prove [A * (B * C) <~> (A * B) * C]

Make use of the new dependent goals feature to make the proof prettier.
Merge pull request #428 from JasonGross/prod-type-assoc

LGTM. I am merging because it is so small and it does not conflict with other stuff.

Prove [A * (B * C) <~> (A * B) * C]
Work around bug 3507

As mentioned in https://coq.inria.fr/bugs/show_bug.cgi?id=3507, this is
unlikely to be fixed in the near future, as it would require radically
changing how Ltac works; see
https://coq.inria.fr/bugs/show_bug.cgi?id=3503#c1.
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
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