The equivR proof rule proves a bi-implication P↔Q by separately assuming its left-hand side P to prove its right-hand side Q and, on a separate branch, assuming its right-hand side Q to prove its left-hand side P.
See also
prop uses all propositional logic rules for operators ¬,∧,∨,→,↔
unfold does all easy steps until loop or ODE without excessive branching