simp only [List.length_pmap]
α : Type u
β : Type v
inst✝³ : BishopFin α
inst✝² : BishopFin β
p q : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
⊢ List.length (List.filter (fun a => decide (p a)) (elems α)) =
    List.length
      (List.pmap Subtype.mk (List.filter (fun a => decide (p a)) (elems α))
        (_ : ∀ (a : α), a ∈ List.filter (fun a => decide (p a)) (elems α) → p a))
no goals