assumption
case h
α : Type u_1
inst✝ : SizeOf α
f : α → Bool
hd : α
tl : List α
ih : ¬filter f tl = tl → sizeOf (filter f tl) < sizeOf tl
x✝ : Bool
hHd : f hd = true
h : ¬filter f tl = tl
⊢ ¬filter f tl = tl
no goals