. rfl
case cons.cons.zero.zero
α : Type u
β : Type v
a : α
l : List α
nodup : Pairwise (fun x x_1 => x ≠ x_1) l
ha : ∀ (a' : α), a' ∈ l → a ≠ a'
IH : ∀ (i j : Nat) {hi : i < length l} {hj : j < length l}, l[i] = l[j] → i = j
hi hj : Nat.zero < length (a :: l)
h : a = a
⊢ Nat.zero = Nat.zero

case cons.cons.zero.succ
α : Type u
β : Type v
a : α
l : List α
nodup : Pairwise (fun x x_1 => x ≠ x_1) l
ha : ∀ (a' : α), a' ∈ l → a ≠ a'
IH : ∀ (i j : Nat) {hi : i < length l} {hj : j < length l}, l[i] = l[j] → i = j
hi : Nat.zero < length (a :: l)
n✝ : Nat
hj : Nat.succ n✝ < length (a :: l)
h : a = get l { val := n✝, isLt := (_ : Nat.succ n✝ ≤ length l) }
⊢ Nat.zero = Nat.succ n✝

case cons.cons.succ.zero
α : Type u
β : Type v
a : α
l : List α
nodup : Pairwise (fun x x_1 => x ≠ x_1) l
ha : ∀ (a' : α), a' ∈ l → a ≠ a'
IH : ∀ (i j : Nat) {hi : i < length l} {hj : j < length l}, l[i] = l[j] → i = j
n✝ : Nat
hi : Nat.succ n✝ < length (a :: l)
hj : Nat.zero < length (a :: l)
h : get l { val := n✝, isLt := (_ : Nat.succ n✝ ≤ length l) } = a
⊢ Nat.succ n✝ = Nat.zero

case cons.cons.succ.succ
α : Type u
β : Type v
a : α
l : List α
nodup : Pairwise (fun x x_1 => x ≠ x_1) l
ha : ∀ (a' : α), a' ∈ l → a ≠ a'
IH : ∀ (i j : Nat) {hi : i < length l} {hj : j < length l}, l[i] = l[j] → i = j
n✝¹ : Nat
hi : Nat.succ n✝¹ < length (a :: l)
n✝ : Nat
hj : Nat.succ n✝ < length (a :: l)
h :
  get l { val := n✝¹, isLt := (_ : Nat.succ n✝¹ ≤ length l) } =
    get l { val := n✝, isLt := (_ : Nat.succ n✝ ≤ length l) }
⊢ Nat.succ n✝¹ = Nat.succ n✝
case cons.cons.zero.succ
α : Type u
β : Type v
a : α
l : List α
nodup : Pairwise (fun x x_1 => x ≠ x_1) l
ha : ∀ (a' : α), a' ∈ l → a ≠ a'
IH : ∀ (i j : Nat) {hi : i < length l} {hj : j < length l}, l[i] = l[j] → i = j
hi : Nat.zero < length (a :: l)
n✝ : Nat
hj : Nat.succ n✝ < length (a :: l)
h : a = get l { val := n✝, isLt := (_ : Nat.succ n✝ ≤ length l) }
⊢ Nat.zero = Nat.succ n✝

case cons.cons.succ.zero
α : Type u
β : Type v
a : α
l : List α
nodup : Pairwise (fun x x_1 => x ≠ x_1) l
ha : ∀ (a' : α), a' ∈ l → a ≠ a'
IH : ∀ (i j : Nat) {hi : i < length l} {hj : j < length l}, l[i] = l[j] → i = j
n✝ : Nat
hi : Nat.succ n✝ < length (a :: l)
hj : Nat.zero < length (a :: l)
h : get l { val := n✝, isLt := (_ : Nat.succ n✝ ≤ length l) } = a
⊢ Nat.succ n✝ = Nat.zero

case cons.cons.succ.succ
α : Type u
β : Type v
a : α
l : List α
nodup : Pairwise (fun x x_1 => x ≠ x_1) l
ha : ∀ (a' : α), a' ∈ l → a ≠ a'
IH : ∀ (i j : Nat) {hi : i < length l} {hj : j < length l}, l[i] = l[j] → i = j
n✝¹ : Nat
hi : Nat.succ n✝¹ < length (a :: l)
n✝ : Nat
hj : Nat.succ n✝ < length (a :: l)
h :
  get l { val := n✝¹, isLt := (_ : Nat.succ n✝¹ ≤ length l) } =
    get l { val := n✝, isLt := (_ : Nat.succ n✝ ≤ length l) }
⊢ Nat.succ n✝¹ = Nat.succ n✝