Theorem: BunchImpl.BunchWithHole.idem_substX (BunchImpl/Term/Bunch.lean)

State before:
P✝ V✝ : Sort u_1
b : Bunch.X P✝ V✝
Γ : X P✝ V✝
⊢ b = substX b Γ ↔ Γ = hole
Tactic:
rw [eq_comm]
State after:
P✝ V✝ : Sort u_1
b : Bunch.X P✝ V✝
Γ : X P✝ V✝
⊢ substX b Γ = b ↔ Γ = hole

State before:
P✝ V✝ : Sort u_1
b : Bunch.X P✝ V✝
Γ : X P✝ V✝
⊢ substX b Γ = b ↔ Γ = hole
Tactic:
simp
State after:
no goals