apply card_le_card_of_inj Subtype.val
α : Type u
p : α → Prop
inst✝¹ : BishopFin α
inst✝ : DecidablePred p
⊢ card { a // p a } ≤ card α
α : Type u
p : α → Prop
inst✝¹ : BishopFin α
inst✝ : DecidablePred p
⊢ ∀ (a₁ a₂ : { a // p a }), a₁.val = a₂.val → a₁ = a₂