m n : ℕ
α : Type u_1
β : Type ?u.5607
γ : Type ?u.5610
P : (Fin 0 → α) → Prop
⊢ P ![] ↔ P finZeroElim
m n : ℕ
α : Type u_1
β : Type ?u.5607
γ : Type ?u.5610
P : (Fin 0 → α) → Prop
⊢ Forall P ↔ ∀ (x : Fin 0 → α), P x
simp only [Forall, Fin.forall_fin_zero_pi]
no goals
m n : ℕ
α : Type u_1
β : Type ?u.5607
γ : Type ?u.5610
P : (Fin 0 → α) → Prop
⊢ P ![] ↔ P finZeroElim
rfl
no goals
m n✝ : ℕ
α : Type u_1
β : Type ?u.5607
γ : Type ?u.5610
n : ℕ
P : (Fin (Nat.succ n) → α) → Prop
⊢ Forall P ↔ ∀ (x : Fin (Nat.succ n) → α), P x
simp only [Forall, forall_iff, Fin.forall_fin_succ_pi, Matrix.vecCons]