rename_i b l
case cons.cons.h
α : Type u
β : Type v
inst✝² : BishopFin α
inst✝¹ : BishopFin β
inst✝ : Subsingleton α
a head✝ : α
tail✝ : List α
hl : elems α = a :: head✝ :: tail✝
⊢ False
case cons.cons.h
α : Type u
β : Type v
inst✝² : BishopFin α
inst✝¹ : BishopFin β
inst✝ : Subsingleton α
a b : α
l : List α
hl : elems α = a :: b :: l
⊢ False