case a.h
n : ℕ
α α' β β' : TypeVec (n + 1)
f : α ⟹ β
f' : α' ⟹ β'
i : Fin2 n
x✝ : drop (α ⊗ α') i
⊢ dropFun (f ⊗' f') i x✝ = (dropFun f ⊗' dropFun f') i x✝
n : ℕ
α α' β β' : TypeVec (n + 1)
f : α ⟹ β
f' : α' ⟹ β'
⊢ dropFun (f ⊗' f') = (dropFun f ⊗' dropFun f')
ext i : 2
no goals
case a.h
n : ℕ
α α' β β' : TypeVec (n + 1)
f : α ⟹ β
f' : α' ⟹ β'
i : Fin2 n
x✝ : drop (α ⊗ α') i
⊢ dropFun (f ⊗' f') i x✝ = (dropFun f ⊗' dropFun f') i x✝
induction i <;> simp [dropFun, *] <;> rfl