Theorem: SciLean.ArrayType.ext (SciLean/Data/ArrayType/Basic.lean)

State before:
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
Tactic:
sorry_proof
State after:
no goals