@[simp]

theorem Part.mem_vector_mOfFn {α : Type u_1} {n : ℕ} {w : List.Vector α n} {v : Fin n →. α} : w ∈ List.Vector.mOfFn v ↔ ∀ (i : Fin n), w.get i ∈ v i

theorem Part.unit_dom_iff (x : Part Unit) : x.Dom ↔ () ∈ x