. case Single x =>
  cases y
  . case Single y =>
    apply False.elim
    apply p
    constructor
    . exists x
    . exists y
  . case Multiple ys => 
    apply children_mult_levels
case Single
y : Packet
a✝ : Nat
p : ¬(IsSingle (Single a✝) ∧ IsSingle y)
⊢ levels (children (Single a✝)) + levels (children y) < level (Single a✝) + level y

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
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