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

State before:
P : Sort u_1
V : Sort u_2
h : X P V
⊢ sizeOf h > 0
Tactic:
induction h <;> simp
State after:
no goals