Supporting results for pointwise provable equality.

@[simp]

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

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