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

State before:
P : Sort u_1
Γ : BunchWithHole P
⊢ Γ.comp hole = Γ
Tactic:
induction Γ <;> simp_all
State after:
no goals