split
α : Type u_1
inst✝ : SizeOf α
f : α → Bool
hd : α
tl : List α
ih : ¬filter f tl = tl → sizeOf (filter f tl) < sizeOf tl
h :
  ¬(match f hd with
      | true => hd :: filter f tl
      | false => filter f tl) =
      hd :: tl
⊢ sizeOf
      (match f hd with
      | true => hd :: filter f tl
      | false => filter f tl) <
    1 + sizeOf hd + sizeOf tl
case h_1
α : Type u_1
inst✝ : SizeOf α
f : α → Bool
hd : α
tl : List α
ih : ¬filter f tl = tl → sizeOf (filter f tl) < sizeOf tl
h :
  ¬(match f hd with
      | true => hd :: filter f tl
      | false => filter f tl) =
      hd :: tl
x✝ : Bool
heq✝ : f hd = true
⊢ sizeOf (hd :: filter f tl) < 1 + sizeOf hd + sizeOf tl

case h_2
α : Type u_1
inst✝ : SizeOf α
f : α → Bool
hd : α
tl : List α
ih : ¬filter f tl = tl → sizeOf (filter f tl) < sizeOf tl
h :
  ¬(match f hd with
      | true => hd :: filter f tl
      | false => filter f tl) =
      hd :: tl
x✝ : Bool
heq✝ : f hd = false
⊢ sizeOf (filter f tl) < 1 + sizeOf hd + sizeOf tl