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

State before:
P : Sort u_1
h1 h2 : BunchWithHole P
b : Bunch P
⊢ ↑(h1.comp h2) b = ↑h1 (↑h2 b)
Tactic:
induction h1 <;> simp_all [comp, FunLike.coe, subst]
State after:
no goals