n : ℕ
α : TypeVec n
β : TypeVec n
f g : α ⟹ β
h : ∀ (i : Fin2 n), f i = g i
⊢ f = g
n : ℕ
α : TypeVec n
β : TypeVec n
f g : α ⟹ β
⊢ (∀ (i : Fin2 n), f i = g i) → f = g
intro h
case h
n : ℕ
α : TypeVec n
β : TypeVec n
f g : α ⟹ β
h : ∀ (i : Fin2 n), f i = g i
i : Fin2 n
⊢ f i = g i
n : ℕ
α : TypeVec n
β : TypeVec n
f g : α ⟹ β
h : ∀ (i : Fin2 n), f i = g i
⊢ f = g
funext i
no goals
case h
n : ℕ
α : TypeVec n
β : TypeVec n
f g : α ⟹ β
h : ∀ (i : Fin2 n), f i = g i
i : Fin2 n
⊢ f i = g i
apply h