. simp [bne, BEq.beq, decide]
  apply decide_eq_false
  intro yex
  let i: Fin (x :: y :: ys).length := ⟨ 0, Nat.zero_lt_succ _ ⟩
  let j: Fin (x :: y :: ys).length := ⟨ 1, Nat.succ_le_succ (Nat.zero_lt_succ _) ⟩
  let h2 := h i j
  simp [List.get] at h2
  apply h2
  rw [yex]
case left
α : Type u_1
da : DecidableEq α
x y : α
ys : List α
h : DifferentList (x :: y :: ys)
⊢ (y != x) = true

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
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