l m✝ n✝ : ℕ
α : Type u_1
β : Type ?u.961
m n : ℕ
P : Matrix (Fin (m + 1)) (Fin n) α → Prop
⊢ (∀ (x : Fin n → α) (x_1 : Matrix (Fin (Nat.add m 0)) (Fin n) α), P (↑of (vecCons x x_1))) ↔
    ∀ (x : Matrix (Fin (m + 1)) (Fin n) α), P x
l m✝ n✝ : ℕ
α : Type u_1
β : Type ?u.961
m n : ℕ
P : Matrix (Fin (m + 1)) (Fin n) α → Prop
⊢ Forall P ↔ ∀ (x : Matrix (Fin (m + 1)) (Fin n) α), P x
simp only [Forall, FinVec.forall_iff, forall_iff]
no goals
l m✝ n✝ : ℕ
α : Type u_1
β : Type ?u.961
m n : ℕ
P : Matrix (Fin (m + 1)) (Fin n) α → Prop
⊢ (∀ (x : Fin n → α) (x_1 : Matrix (Fin (Nat.add m 0)) (Fin n) α), P (↑of (vecCons x x_1))) ↔
    ∀ (x : Matrix (Fin (m + 1)) (Fin n) α), P x
exact Iff.symm Fin.forall_fin_succ_pi