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

State before:
P : Type u_1
Γ : BunchWithHole P
b : Bunch P
⊢ sorryAx Prop true ↔ sorryAx Prop true
Tactic:
simp [FunLike.coe]
State after:
no goals