dsimp [card]
α : Type u
β : Type v
inst✝² : BishopFin α
inst✝¹ : BishopFin β
inst✝ : Subsingleton α
⊢ card α ≤ 1
α : Type u
β : Type v
inst✝² : BishopFin α
inst✝¹ : BishopFin β
inst✝ : Subsingleton α
⊢ List.length (elems α) ≤ 1