simp
case cons.h_1
α : Type u_1
inst✝ : SizeOf α
f : α → Bool
head✝ : α
tail✝ : List α
tail_ih✝ : sizeOf (filter f tail✝) ≤ sizeOf tail✝
x✝ : Bool
heq✝ : f head✝ = true
⊢ sizeOf (head✝ :: filter f tail✝) ≤ 1 + sizeOf head✝ + sizeOf tail✝
case cons.h_1
α : Type u_1
inst✝ : SizeOf α
f : α → Bool
head✝ : α
tail✝ : List α
tail_ih✝ : sizeOf (filter f tail✝) ≤ sizeOf tail✝
x✝ : Bool
heq✝ : f head✝ = true
⊢ 1 + sizeOf head✝ + sizeOf (filter f tail✝) ≤ 1 + sizeOf head✝ + sizeOf tail✝