simp only [sieve, List.sieve]
η : Type u_η
dec_η : DecidableEq η
schema : Schema
τ : Type u_1
bs : List Bool
xs : List τ
head✝ : Bool
tail✝ : List Bool
⊢ sieve (head✝ :: tail✝) [] = List.sieve (head✝ :: tail✝) []
no goals