Greatly improved Record tactics, thanks to help from Jason Gross

The issig tactics now:
1. Don't require passing the fibration as an argument
2. All have the same name
3. Build coherent equivalences directly, rather than with adjointify
4. Are a bit faster
5. Incorporate more Ltac black magic.