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]