apply congrArg (λ x => x + 1)
α : Type u_1
bs : List Bool
x : α
xs : List α
h : length (true :: bs) = length (x :: xs)
ih : length (sieve bs xs) = length (removeAllEq bs [false])
⊢ length (sieve bs xs) + 1 = length (removeAllEq bs [false]) + 1
α : Type u_1
bs : List Bool
x : α
xs : List α
h : length (true :: bs) = length (x :: xs)
ih : length (sieve bs xs) = length (removeAllEq bs [false])
⊢ length (sieve bs xs) = length (removeAllEq bs [false])