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

State before:
a b : Nat
⊢ Equiv empty a b ↔ a = b
Tactic:
simp [Equiv]
State after:
no goals