Merge pull request #427 from JasonGross/implicit-equiv

Mark the arguments to Equiv projections implicit
Work around bug 3507

As mentioned in https://coq.inria.fr/bugs/show_bug.cgi?id=3507, this is
unlikely to be fixed in the near future, as it would require radically
changing how Ltac works; see
https://coq.inria.fr/bugs/show_bug.cgi?id=3503#c1.
WIP
Take advantage of judgmental eta to clean up