cases i <;> cases j <;> simp at hxij ⊢
case cons.mp.mk.mk
α : Type u
inst✝ : DecidableEq α
a : α
x : Array α
h : ¬a ∈ x ∧ ∀ (i j : Fin (size x)), x[↑i] = x[↑j] → i = j
i : Nat
hi : i < size (cons a x)
j : Nat
hj : j < size (cons a x)
hxij : (cons a x)[↑{ val := i, isLt := hi }] = (cons a x)[↑{ val := j, isLt := hj }]
⊢ { val := i, isLt := hi } = { val := j, isLt := hj }
case cons.mp.mk.mk.zero.succ
α : Type u
inst✝ : DecidableEq α
a : α
x : Array α
h : ¬a ∈ x ∧ ∀ (i j : Fin (size x)), x[↑i] = x[↑j] → i = j
hi : Nat.zero < size (cons a x)
n✝ : Nat
hj : Nat.succ n✝ < size (cons a x)
hxij : a = x[n✝]
⊢ 0 = { val := Nat.succ n✝, isLt := hj }

case cons.mp.mk.mk.succ.zero
α : Type u
inst✝ : DecidableEq α
a : α
x : Array α
h : ¬a ∈ x ∧ ∀ (i j : Fin (size x)), x[↑i] = x[↑j] → i = j
n✝ : Nat
hi : Nat.succ n✝ < size (cons a x)
hj : Nat.zero < size (cons a x)
hxij : x[n✝] = a
⊢ { val := Nat.succ n✝, isLt := hi } = 0

case cons.mp.mk.mk.succ.succ
α : Type u
inst✝ : DecidableEq α
a : α
x : Array α
h : ¬a ∈ x ∧ ∀ (i j : Fin (size x)), x[↑i] = x[↑j] → i = j
n✝¹ : Nat
hi : Nat.succ n✝¹ < size (cons a x)
n✝ : Nat
hj : Nat.succ n✝ < size (cons a x)
hxij : x[n✝¹] = x[n✝]
⊢ n✝¹ = n✝