. apply DifListHead
  apply DifListTail y
  apply DifListShuffle
  exact h
case right
α : Type u_1
da : DecidableEq α
x y : α
ys : List α
h : DifferentList (x :: y :: ys)
⊢ List.foldr (fun a r => a != x && r) true ys = true
no goals