Equivalence vs. Equality - Generalized Rewriting

Currently, the bidirectional entailment ⊣⊢ is defined as equality in order to use Lean's rw tactic to rewrite with bidirectional entailments in proofs inside the framework (e.g. in proofs of the derived laws).
https://github.com/larsk21/iris-lean/blob/bde762e5d24b2f3777b8c950dc5857b2e8f4f9c6/src/Iris/BI/DerivedConnectives.lean#L7

This requires the axiom equiv_entails, stating that equality is equal to entailments in both directions, which is used to resolve a bidirectional entailment (using an instance of AntiSymm).
https://github.com/larsk21/iris-lean/blob/bde762e5d24b2f3777b8c950dc5857b2e8f4f9c6/src/Iris/BI/Interface.lean#L108-L111

The axiom is however not true for all separation logics, which is why setoids and quotient types need to be used to instantiate the separation logic interface with such logics (see readme). This is, however, not a viable solution, since Lean's Setoid type does not support parameterized equivalances, such as ={n}= from the Iris separation logic.

There are at least two possible solutions:

1. As soon as Lean supports generalized rewriting, we should change the equality = to an equivalence ≡ and rewrite with that.
2. We could instead extend the tactic rw' included in this project (currently used for rewriting with preorders, such as ⊢) to support equivalences as well. This is less prefered, since it would probably require a backtracking search and should really be part of a general solution for generalized rewriting outside of this project. Also, rw' should be replaced with Lean's generalized rewriting in the future.

see also Rewriting congruent relations

Read src/Iris/BI/DerivedConnectives.lean around the ⊣⊢ definition and src/Iris/BI/Interface.lean around equiv_entails. Then review the existing rw' tactic and the linked generalized-rewriting discussion to compare the proposed approaches. Done means selecting and implementing a sound rewriting design that avoids requiring equiv_entails for separation logics with parameterized equivalences.