case h
n : ℕ
α α' β β' : TypeVec n
f : α ⟹ β
g : α' ⟹ β'
i : Fin2 n
⊢ (prod.snd ⊚ (f ⊗' g)) i = (g ⊚ prod.snd) i
n : ℕ
α α' β β' : TypeVec n
f : α ⟹ β
g : α' ⟹ β'
⊢ prod.snd ⊚ (f ⊗' g) = g ⊚ prod.snd
funext i
case h.fz
n n✝ : ℕ
α α' β β' : TypeVec (succ n✝)
f : α ⟹ β
g : α' ⟹ β'
⊢ (prod.snd ⊚ (f ⊗' g)) Fin2.fz = (g ⊚ prod.snd) Fin2.fz

case h.fs
n n✝ : ℕ
a✝ : Fin2 n✝
a_ih✝ : ∀ {α α' β β' : TypeVec n✝} (f : α ⟹ β) (g : α' ⟹ β'), (prod.snd ⊚ (f ⊗' g)) a✝ = (g ⊚ prod.snd) a✝
α α' β β' : TypeVec (succ n✝)
f : α ⟹ β
g : α' ⟹ β'
⊢ (prod.snd ⊚ (f ⊗' g)) (Fin2.fs a✝) = (g ⊚ prod.snd) (Fin2.fs a✝)
case h
n : ℕ
α α' β β' : TypeVec n
f : α ⟹ β
g : α' ⟹ β'
i : Fin2 n
⊢ (prod.snd ⊚ (f ⊗' g)) i = (g ⊚ prod.snd) i
induction i
case h.fs
n n✝ : ℕ
a✝ : Fin2 n✝
a_ih✝ : ∀ {α α' β β' : TypeVec n✝} (f : α ⟹ β) (g : α' ⟹ β'), (prod.snd ⊚ (f ⊗' g)) a✝ = (g ⊚ prod.snd) a✝
α α' β β' : TypeVec (succ n✝)
f : α ⟹ β
g : α' ⟹ β'
⊢ (prod.snd ⊚ (f ⊗' g)) (Fin2.fs a✝) = (g ⊚ prod.snd) (Fin2.fs a✝)
case h.fz
n n✝ : ℕ
α α' β β' : TypeVec (succ n✝)
f : α ⟹ β
g : α' ⟹ β'
⊢ (prod.snd ⊚ (f ⊗' g)) Fin2.fz = (g ⊚ prod.snd) Fin2.fz

case h.fs
n n✝ : ℕ
a✝ : Fin2 n✝
a_ih✝ : ∀ {α α' β β' : TypeVec n✝} (f : α ⟹ β) (g : α' ⟹ β'), (prod.snd ⊚ (f ⊗' g)) a✝ = (g ⊚ prod.snd) a✝
α α' β β' : TypeVec (succ n✝)
f : α ⟹ β
g : α' ⟹ β'
⊢ (prod.snd ⊚ (f ⊗' g)) (Fin2.fs a✝) = (g ⊚ prod.snd) (Fin2.fs a✝)
case fz => rfl
no goals
case h.fs
n n✝ : ℕ
a✝ : Fin2 n✝
a_ih✝ : ∀ {α α' β β' : TypeVec n✝} (f : α ⟹ β) (g : α' ⟹ β'), (prod.snd ⊚ (f ⊗' g)) a✝ = (g ⊚ prod.snd) a✝
α α' β β' : TypeVec (succ n✝)
f : α ⟹ β
g : α' ⟹ β'
⊢ (prod.snd ⊚ (f ⊗' g)) (Fin2.fs a✝) = (g ⊚ prod.snd) (Fin2.fs a✝)
case fs _ _ i_ih => apply i_ih
no goals
n n✝ : ℕ
α α' β β' : TypeVec (succ n✝)
f : α ⟹ β
g : α' ⟹ β'
⊢ (prod.snd ⊚ (f ⊗' g)) Fin2.fz = (g ⊚ prod.snd) Fin2.fz
rfl
no goals
n n✝ : ℕ
a✝ : Fin2 n✝
i_ih : ∀ {α α' β β' : TypeVec n✝} (f : α ⟹ β) (g : α' ⟹ β'), (prod.snd ⊚ (f ⊗' g)) a✝ = (g ⊚ prod.snd) a✝
α α' β β' : TypeVec (succ n✝)
f : α ⟹ β
g : α' ⟹ β'
⊢ (prod.snd ⊚ (f ⊗' g)) (Fin2.fs a✝) = (g ⊚ prod.snd) (Fin2.fs a✝)
apply i_ih