cases x <;> simp [children, levels, level]
x : Packet
ys : List Packet
⊢ levels (children x) + levels ys < level x + level (Multiple ys)
case Single
ys : List Packet
a✝ : Nat
⊢ 1 + levels ys < levels ys + 2

case Multiple
ys a✝ : List Packet
⊢ levels a✝ + levels ys < levels a✝ + 2 + (levels ys + 2)