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

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