cases hl : elems α <;> dsimp
α : Type u
β : Type v
inst✝² : BishopFin α
inst✝¹ : BishopFin β
inst✝ : Subsingleton α
⊢ List.length (elems α) ≤ 1
case nil
α : Type u
β : Type v
inst✝² : BishopFin α
inst✝¹ : BishopFin β
inst✝ : Subsingleton α
hl : elems α = []
⊢ 0 ≤ 1

case cons
α : Type u
β : Type v
inst✝² : BishopFin α
inst✝¹ : BishopFin β
inst✝ : Subsingleton α
head✝ : α
tail✝ : List α
hl : elems α = head✝ :: tail✝
⊢ Nat.succ (List.length tail✝) ≤ 1