exact this.head (List.mem_cons_self a l)
case cons.cons.h.refl
α : Type u
β : Type v
inst✝² : BishopFin α
inst✝¹ : BishopFin β
inst✝ : Subsingleton α
a : α
l : List α
hl : elems α = a :: a :: l
this : List.Nodup (a :: a :: l)
⊢ False
no goals