. apply DifListHead dl
case left
α : Type u_1
inst✝ : DecidableEq α
h : α
t : List α
dl : DifferentList (h :: t)
⊢ (List.all t fun x => x != h) = true

case right
α : Type u_1
inst✝ : DecidableEq α
h : α
t : List α
dl : DifferentList (h :: t)
⊢ differs t = true
case right
α : Type u_1
inst✝ : DecidableEq α
h : α
t : List α
dl : DifferentList (h :: t)
⊢ differs t = true