HoTT/HoTT — pull request #428 by JasonGross (2014-08-22 17:22:58+00:00)
Title: Prove [A * (B * C) <~> (A * B) * C]

Make use of the new dependent goals feature to make the proof prettier.