no goals
α : Type u
β : Type v
p : α → Prop
inst✝ : DecidablePred p
as : List α
⊢ indexesValues (fun b => decide (p b)) as = filter ((fun b => decide (p b)) ∘ Prod.snd) (enum as)
simp [indexesValues, foldrIdx_eq_foldr_enum, uncurry, filter_eq_foldr]