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

State before:
P : Sort u_1
b : Bunch P
h : BunchWithHole P
⊢ sizeOf (subst b h) = sizeOf b + sizeOf h - 1
Tactic:
induction h <;> simp [subst, *] <;> sorry
State after:
no goals