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

case Multiple
x : Nat
a✝ : List Packet
p : ¬(IsSingle (Single x) ∧ IsSingle (Multiple a✝))
⊢ levels (children (Single x)) + levels (children (Multiple a✝)) < level (Single x) + level (Multiple a✝)
case Multiple
x : Nat
a✝ : List Packet
p : ¬(IsSingle (Single x) ∧ IsSingle (Multiple a✝))
⊢ levels (children (Single x)) + levels (children (Multiple a✝)) < level (Single x) + level (Multiple a✝)