. intro h
  constructor
  . intro hmem
    have ⟨i,hi, hxi⟩ := mem_iff_get.mp hmem
    specialize h ⟨i+1, Nat.succ_lt_succ hi⟩ ⟨0, x.size.zero_lt_succ⟩ hxi
    cases h
  . intro i j
    specialize h i.succ j.succ
    simp only [size_cons, Fin.val_succ, getElem_cons_succ, Fin.succ_inj] at h
    exact h
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
no goals