rintro rfl
case mp
α : Type u_1
A B : Array α
h : A.size = B.size
⊢ A = B → ∀ (i : ℕ) (h1 : i < A.size) (h2 : i < B.size), A[i] = B[i]
case mp
α : Type u_1
A : Array α
h : A.size = A.size
⊢ ∀ (i : ℕ) (h1 h2 : i < A.size), A[i] = A[i]