Work around bug 3583

This is https://coq.inria.fr/bugs/show_bug.cgi?id=3583, "Error: Ltac
variable x is not bound to an identifier. It cannot be used in a
binder." should not trigger when the binder is shared with one in the
pattern match
Work around bug 3587

This is https://coq.inria.fr/bugs/show_bug.cgi?id=3587, [rewrite] fails
to simplify away primitive projections even though it simplifies away
non-primitive projections
Add sig as a primitive record
Work around an as-yet-unspecified bug in theories/hit/Connectedness.v
Take advantage of eta to clean sigma proofs

Now they use less funext