refactor: retire setoids

[Kaptch]

Description

Pass over deprecating equiv in favor of eq. The remaining task is a small cleanup. I've tried to keep this one minimal by preserving the proofs as much as possible, while eliminating equiv in signatures. I'll make a pass over proofs in a separate PR.

[Kaptch]

Short summary: deprecated OFE.Equiv, maps to/from equality, congruence rules wrt OFE.Equiv, then went fixing the downstream proofs, until none of the code is using those. At this point, OFE.Equiv should be safely deleted (can also do it now, but I would wait a week or two in case any downstream project continues to use it).
I tried to preserve all signatures by just changing OFE.Equiv to equality. The only naming changes come from congruence rules for BigOps, because they combine extensionality and congruence. There, I made a pass to merge some lemmas.

The proofs are mostly the same, and I'll make a separate pass to use simp/rw in them instead of manual chains of equalities.
I can also split the PR a bit, but it seems that is the cleanest way to change all signatures in one go to avoid to_eq/from_eq casting.

[markusdemedeiros]

Don't worry about breaking downstream projects (a week or two changes nothing since they should be using the versioned releases anyways). I'll do my best to review this promptly!