HoTT/HoTT — pull request #518 by mikeshulman (2014-09-19 14:10:57+00:00)
Title: Prove that O preserves products without funext and without tactics

In place of #515