cases xs
α : Type u_1
inst✝ : DecidableEq α
xs : List α
p : differs xs = true
⊢ DifferentList xs
case nil
α : Type u_1
inst✝ : DecidableEq α
p : differs [] = true
⊢ DifferentList []

case cons
α : Type u_1
inst✝ : DecidableEq α
head✝ : α
tail✝ : List α
p : differs (head✝ :: tail✝) = true
⊢ DifferentList (head✝ :: tail✝)