contradiction
α : Type u_1
inst✝ : DecidableEq α
h : α
t : List α
p : differs (h :: t) = true
ilt : Nat.zero < List.length (h :: t)
j : Nat
jlt : Nat.succ j < List.length (h :: t)
iej : h = List.get t { val := j, isLt := (_ : Nat.succ j ≤ List.length t) }
xs : False := differsHead p iej
⊢ Nat.zero = Nat.succ j
no goals