simp only
case cons.false
α : Type u_1
g : α → Bool
x : α
xs : List α
ih : length (filter g xs) ≤ length xs
⊢ length
      (match false with
      | true => x :: filter g xs
      | false => filter g xs) ≤
    length (x :: xs)
case cons.false
α : Type u_1
g : α → Bool
x : α
xs : List α
ih : length (filter g xs) ≤ length xs
⊢ length (filter g xs) ≤ length (x :: xs)