apply Nat.le.refl
case cons.true
α : Type u_1
g : α → Bool
x : α
xs : List α
ih : ∀ (rs : List α), length (filterTR.loop g xs rs) ≤ length xs + length rs
rs : List α
⊢ length xs + (1 + length rs) ≤ length xs + (1 + length rs)
no goals