cases xs
α : Type u_1
da : DecidableEq α
x : α
xs : List α
h : DifferentList (x :: xs)
⊢ (List.all xs fun x_1 => x_1 != x) = true
case nil
α : Type u_1
da : DecidableEq α
x : α
h : DifferentList [x]
⊢ (List.all [] fun x_1 => x_1 != x) = true

case cons
α : Type u_1
da : DecidableEq α
x head✝ : α
tail✝ : List α
h : DifferentList (x :: head✝ :: tail✝)
⊢ (List.all (head✝ :: tail✝) fun x_1 => x_1 != x) = true