. intro h i j hxij
  rcases i with ⟨i,hi⟩; rcases j with ⟨j,hj⟩
  cases i <;> cases j <;> simp at hxij ⊢
  . exfalso; apply h.1
    rewrite [hxij]; exact getElem_mem x _
  . exfalso; apply h.1
    rewrite [← hxij]; exact getElem_mem x _
  . exact Fin.val_eq_of_eq <| h.2 ⟨_, Nat.lt_of_succ_lt_succ hi⟩ ⟨_, Nat.lt_of_succ_lt_succ hj⟩ hxij
case cons.mp
α : Type u
inst✝ : DecidableEq α
a : α
x : Array α
⊢ (¬a ∈ x ∧ ∀ (i j : Fin (size x)), x[↑i] = x[↑j] → i = j) →
    ∀ (i j : Fin (size (cons a x))), (cons a x)[↑i] = (cons a x)[↑j] → i = j

case cons.mpr
α : Type u
inst✝ : DecidableEq α
a : α
x : Array α
⊢ (∀ (i j : Fin (size (cons a x))), (cons a x)[↑i] = (cons a x)[↑j] → i = j) →
    ¬a ∈ x ∧ ∀ (i j : Fin (size x)), x[↑i] = x[↑j] → i = j
case cons.mpr
α : Type u
inst✝ : DecidableEq α
a : α
x : Array α
⊢ (∀ (i j : Fin (size (cons a x))), (cons a x)[↑i] = (cons a x)[↑j] → i = j) →
    ¬a ∈ x ∧ ∀ (i j : Fin (size x)), x[↑i] = x[↑j] → i = j