induction L <;> simp [filter]
α : Type u_1
inst✝ : SizeOf α
f : α → Bool
L : List α
⊢ sizeOf (filter f L) ≤ sizeOf L
case cons
α : Type u_1
inst✝ : SizeOf α
f : α → Bool
head✝ : α
tail✝ : List α
tail_ih✝ : sizeOf (filter f tail✝) ≤ sizeOf tail✝
⊢ sizeOf
      (match f head✝ with
      | true => head✝ :: filter f tail✝
      | false => filter f tail✝) ≤
    1 + sizeOf head✝ + sizeOf tail✝