. case Multiple xs => 
  conv => 
    rhs
    rw [Nat.add_assoc]
    conv => 
      rhs
      rw [← Nat.add_assoc]
      conv => 
        lhs
        rw [Nat.add_comm]  
      rw [Nat.add_assoc]
      simp [Nat.add]
    rw [←Nat.add_assoc]
  apply @Nat.add_lt_add_left 0
  apply Nat.zero_lt_succ
case Multiple
ys a✝ : List Packet
⊢ levels a✝ + levels ys < levels a✝ + 2 + (levels ys + 2)
no goals