rename_i a l
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
case cons
α : Type u
β : Type v
inst✝² : BishopFin α
inst✝¹ : BishopFin β
inst✝ : Subsingleton α
a : α
l : List α
hl : elems α = a :: l
⊢ Nat.succ (List.length l) ≤ 1