Theorem: Matrix.forall_iff (Arithmetization/Vorspiel/Vorspiel.lean)

State before:
α : Type u_1
n : ℕ
p : (Fin (n + 1) → α) → Prop
h : ∀ (a : α) (v : Fin n → α), p (a :> v)
v : Fin (n + 1) → α
⊢ p v
Tactic:
simpa [←eq_vecCons v] using h (v 0) (v ∘ Fin.succ)
State after:
no goals