n : ℕ
α : TypeVec (n + 1)
β : TypeVec (n + 1)
f g : α ⟹ β
h₀ : dropFun f = dropFun g
h₁ : lastFun f = lastFun g
x : Fin2 (n + 1)
⊢ f x = g x
n : ℕ
α : TypeVec (n + 1)
β : TypeVec (n + 1)
f g : α ⟹ β
h₀ : dropFun f = dropFun g
h₁ : lastFun f = lastFun g
⊢ f = g
refine funext (fun x => ?_)
case fz
n : ℕ
α : TypeVec (n + 1)
β : TypeVec (n + 1)
f g : α ⟹ β
h₀ : dropFun f = dropFun g
h₁ : lastFun f = lastFun g
⊢ f Fin2.fz = g Fin2.fz

case fs
n : ℕ
α : TypeVec (n + 1)
β : TypeVec (n + 1)
f g : α ⟹ β
h₀ : dropFun f = dropFun g
h₁ : lastFun f = lastFun g
a✝ : Fin2 (Nat.add n 0)
⊢ f (Fin2.fs a✝) = g (Fin2.fs a✝)
n : ℕ
α : TypeVec (n + 1)
β : TypeVec (n + 1)
f g : α ⟹ β
h₀ : dropFun f = dropFun g
h₁ : lastFun f = lastFun g
x : Fin2 (n + 1)
⊢ f x = g x
cases x
case fs
n : ℕ
α : TypeVec (n + 1)
β : TypeVec (n + 1)
f g : α ⟹ β
h₀ : dropFun f = dropFun g
h₁ : lastFun f = lastFun g
a✝ : Fin2 (Nat.add n 0)
⊢ f (Fin2.fs a✝) = g (Fin2.fs a✝)
case fz
n : ℕ
α : TypeVec (n + 1)
β : TypeVec (n + 1)
f g : α ⟹ β
h₀ : dropFun f = dropFun g
h₁ : lastFun f = lastFun g
⊢ f Fin2.fz = g Fin2.fz

case fs
n : ℕ
α : TypeVec (n + 1)
β : TypeVec (n + 1)
f g : α ⟹ β
h₀ : dropFun f = dropFun g
h₁ : lastFun f = lastFun g
a✝ : Fin2 (Nat.add n 0)
⊢ f (Fin2.fs a✝) = g (Fin2.fs a✝)
. apply h₁
no goals
case fs
n : ℕ
α : TypeVec (n + 1)
β : TypeVec (n + 1)
f g : α ⟹ β
h₀ : dropFun f = dropFun g
h₁ : lastFun f = lastFun g
a✝ : Fin2 (Nat.add n 0)
⊢ f (Fin2.fs a✝) = g (Fin2.fs a✝)
. apply congr_fun h₀
no goals
case fz
n : ℕ
α : TypeVec (n + 1)
β : TypeVec (n + 1)
f g : α ⟹ β
h₀ : dropFun f = dropFun g
h₁ : lastFun f = lastFun g
⊢ f Fin2.fz = g Fin2.fz
apply h₁
no goals
case fs
n : ℕ
α : TypeVec (n + 1)
β : TypeVec (n + 1)
f g : α ⟹ β
h₀ : dropFun f = dropFun g
h₁ : lastFun f = lastFun g
a✝ : Fin2 (Nat.add n 0)
⊢ f (Fin2.fs a✝) = g (Fin2.fs a✝)
apply congr_fun h₀