Theorem: BunchImpl.BunchWithHole.idem_subst (BunchImpl/Bunch.lean)

State before:
P✝ : Sort u_1
b : Bunch P✝
Γ : BunchWithHole P✝
⊢ b = subst b Γ ↔ Γ = hole
Tactic:
rw [eq_comm]
State after:
P✝ : Sort u_1
b : Bunch P✝
Γ : BunchWithHole P✝
⊢ subst b Γ = b ↔ Γ = hole

State before:
P✝ : Sort u_1
b : Bunch P✝
Γ : BunchWithHole P✝
⊢ subst b Γ = b ↔ Γ = hole
Tactic:
simp
State after:
no goals