. case Single x => 
  rw [Nat.add_comm]
  apply Nat.lt_succ_self
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)
case Multiple
ys a✝ : List Packet
⊢ levels a✝ + levels ys < levels a✝ + 2 + (levels ys + 2)