Theorem: BunchImpl.BunchWithHole.idem' (BunchImpl/Bunch.lean)

State before:
P : Sort u_1
Γ : BunchWithHole P
b : Bunch P
⊢ b = ↑Γ b ↔ Γ = hole
Tactic:
simp [FunLike.coe]
State after:
no goals