English
Composition on TypeVec arrows respects splitFun: splitFun (f1 ∘ f0) (g1 ∘ g0) equals the composition of splits.
Русский
Композиция стрел на TypeVec согласуется с разделением: splitFun (f1 ∘ f0) (g1 ∘ g0) = splitFun f1 g1 ∘ splitFun f0 g0.
LaTeX
$$$\mathrm{splitFun}(\mathrm{f1} \circ \mathrm{f0})(\mathrm{g1} \circ \mathrm{g0}) = \mathrm{splitFun}(\mathrm{f1} \ g1)(\mathrm{splitFun} f0 g0)$$$
Lean4
theorem splitFun_comp {α₀ α₁ α₂ : TypeVec (n + 1)} (f₀ : drop α₀ ⟹ drop α₁) (f₁ : drop α₁ ⟹ drop α₂)
(g₀ : last α₀ → last α₁) (g₁ : last α₁ → last α₂) :
splitFun (f₁ ⊚ f₀) (g₁ ∘ g₀) = splitFun f₁ g₁ ⊚ splitFun f₀ g₀ :=
eq_of_drop_last_eq rfl rfl
