sorry_proof
Cont : Type u_2
Idx : outParam (Type u_3)
Elem : outParam (Type u_1)
inst✝³ : IndexType Idx
inst✝² : outParam (DecidableEq Idx)
inst✝¹ : LawfulIndexType Idx
inst✝ : ArrayType Cont Idx Elem
x y : Cont
⊢ (∀ (i : Idx), x[i] = y[i]) → x = y
no goals