Theorem: BunchImpl.BunchWithHole.sizeOf_substX (BunchImpl/Term/Bunch.lean)

State before:
P V : Sort u_1
b : Bunch.X P V
h : X P V
⊢ sizeOf (substX b h) = sizeOf b + sizeOf h - 1
Tactic:
induction h <;> simp [subst, substX, comma, semi, instSizeOfBunch] at * <;>
  simp [*] <;> sorry
State after:
no goals