apply Bool.noConfusion
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
no goals