rw [removeAllEq_singleton_hd_neq]
α : 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 (true :: bs) (x :: xs)) = length (removeAllEq (true :: bs) [false])
α : 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 (true :: bs) (x :: xs)) = length (true :: removeAllEq bs [false])

case a
α : 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])
⊢ true ≠ false