Prove that O preserves products without funext
Delete minus1Trunc.v, close #434
Work around bug 3638

This is https://coq.inria.fr/bugs/show_bug.cgi?id=3638, "Anomaly: Bad
recursive type. Please report." on [set]ting an evar involving
primitive projections
Remove dead code
easy lemma `issurj` for defining surjections
Add more documentation to tactics in ReflectiveSubuniverse
change equiv_tr to tr
isequiv_surj_emb
BuildIsSurjection
extrafancy tactic is unnecessary
Revert other fancy tactic
check for truncatedness of the goal in strip_truncations
Merge pull request #513 from mikeshulman/minus1trunc

Delete minus1Trunc.v, close #434
Merge pull request #518 from mikeshulman/refl-subu-prod

Prove that O preserves products without funext and without tactics