theorem Fin.forall_le_vec_iff_forall_le_forall_vec {α : Type u_1} {k : ℕ} [LE α] {P : (Fin (k + 1) → α) → Prop} {f : Fin (k + 1) → α} : (∀ v ≤ f, P v) ↔ ∀ x ≤ f 0, ∀ v ≤ fun (x : Fin k) => f x.succ, P (x :> v)

theorem Fin.forall_vec_iff_forall_forall_vec {k : ℕ} {α : Type u_1} {P : (Fin (k + 1) → α) → Prop} : (∀ (v : Fin (k + 1) → α), P v) ↔ ∀ (x : α) (v : Fin k → α), P (x :> v)

theorem Fin.exists_vec_iff_exists_exists_vec {k : ℕ} {α : Type u_1} {P : (Fin (k + 1) → α) → Prop} : (∃ (v : Fin (k + 1) → α), P v) ↔ ∃ (x : α) (v : Fin k → α), P (x :> v)

theorem Fin.exists_le_vec_iff_exists_le_exists_vec {α : Type u_1} {k : ℕ} [LE α] {P : (Fin (k + 1) → α) → Prop} {f : Fin (k + 1) → α} : (∃ v ≤ f, P v) ↔ ∃ x ≤ f 0, ∃ v ≤ fun (x : Fin k) => f x.succ, P (x :> v)