cases xs <;> simp [differs]
α : Type u_1
inst✝ : DecidableEq α
xs : List α
dl : DifferentList xs
⊢ differs xs = true
case cons
α : Type u_1
inst✝ : DecidableEq α
head✝ : α
tail✝ : List α
dl : DifferentList (head✝ :: tail✝)
⊢ (List.all tail✝ fun x => x != head✝) = true ∧ differs tail✝ = true