Theorem: Lean4Lean.UnionFind.equiv_root_r (Lean4Lean/Verify/UnionFind.lean)

State before:
self : UnionFind
a b : Nat
⊢ Equiv self a (root self b) ↔ Equiv self a b
Tactic:
simp [Equiv, root_root]
State after:
no goals