Theorem: BunchImpl.Subbunch.subst_hole (BunchImpl/Subbunch.lean)

State before:
P : Sort u_1
b : Bunch P
Γ : BunchWithHole P
⊢ Subbunch (↑Γ b) b
Tactic:
induction Γ <;> simp [*]
State after:
no goals