Prove that O preserves products without funext and without tactics

In place of #515