vectorAll_iff_forall

theorem vectorAll_iff_forall : ∀ {α : Type u_1} {n : ℕ} (f : Vector3 α n → Prop), VectorAll n f ↔ ∀ (v : Vector3 α n), f v

This theorem states that for any type `α`, natural number `n`, and a property `f` that takes a vector of length `n` with elements of type `α`, the property `VectorAll n f` is equivalent to saying that for all vectors `v` of length `n` with elements of type `α`, the property `f` holds for `v`. In other words, it's proving that the "curried" version of the universal quantifier (represented by `VectorAll`) over vectors is equivalent to the standard universal quantifier over vectors.

More concisely: For any type `α`, natural number `n`, and property `f` on vectors of length `n` with elements of type `α`, `VectorAll n f` is equivalent to `∀v: Vector α n, f v`.