simp [List.all, List.foldr]
α : Type u_1
da : DecidableEq α
x y : α
ys : List α
h : DifferentList (x :: y :: ys)
⊢ (List.all (y :: ys) fun x_1 => x_1 != x) = true
α : Type u_1
da : DecidableEq α
x y : α
ys : List α
h : DifferentList (x :: y :: ys)
⊢ (y != x) = true ∧ List.foldr (fun a r => a != x && r) true ys = true