theorem Array.exists_of_uset {α : Type u_1} (self : Array α) (i : USize) (d : α) (h : i.toNat < self.size) : ∃ (l₁ : List α), ∃ (l₂ : List α), self.data = l₁ ++ self[i] :: l₂ ∧ l₁.length = i.toNat ∧ (self.uset i d h).data = l₁ ++ d :: l₂