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