. case Multiple xs =>
    conv => 
      lhs
      rw [Nat.add_comm] 
    conv => 
      rhs
      rw [Nat.add_comm] 
    apply children_mult_levels
case Multiple
y : Packet
a✝ : List Packet
p : ¬(IsSingle (Multiple a✝) ∧ IsSingle y)
⊢ levels (children (Multiple a✝)) + levels (children y) < level (Multiple a✝) + level y
no goals