apply children_mult_levels
x : Nat
ys : List Packet
p : ¬(IsSingle (Single x) ∧ IsSingle (Multiple ys))
⊢ levels (children (Single x)) + levels (children (Multiple ys)) < level (Single x) + level (Multiple ys)
no goals