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

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