The equivL proof rule uses a bi-implication P↔Q among its assumptions byy separately assuming both P and Q or, on a separate branch, assuming both ¬P and ¬Q since, after all, both are equivalent.
See also
prop uses all propositional logic rules for operators ¬,∧,∨,→,↔
unfold does all easy steps until loop or ODE without excessive branching