all_goals
  intro h i j hxij
  rcases i with ⟨i,hi⟩; rcases j with ⟨j,hj⟩
  specialize h ⟨i, x.size_eq.symm ▸ hi⟩ ⟨j, x.size_eq.symm ▸ hj⟩ hxij
  cases h; rfl
case mp
α : Type u
n : Nat
inst✝ : DecidableEq α
x : SizedArray α n
⊢ (∀ (i j : Fin (Array.size x.val)), x.val[↑i] = x.val[↑j] → i = j) → ∀ (i j : Fin n), x[↑i] = x[↑j] → i = j

case mpr
α : Type u
n : Nat
inst✝ : DecidableEq α
x : SizedArray α n
⊢ (∀ (i j : Fin n), x[↑i] = x[↑j] → i = j) → ∀ (i j : Fin (Array.size x.val)), x.val[↑i] = x.val[↑j] → i = j
no goals