Mark the arguments to Equiv projections implicit

This is required for pattern matching on primitive projections to work
(which I hope we'll be moving to soon) (see
https://coq.inria.fr/bugs/show_bug.cgi?id=3503), and also seems nicer;
we generally don't need to talk about the type arguments to [equiv_fun]
and [equiv_isequiv].