. case cons y ys => 
  simp [List.all, List.foldr]
  constructor
  . 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]
  . apply DifListHead
    apply DifListTail y
    apply DifListShuffle
    exact h
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
no goals