English
Let P be a multivariate polynomial functor of arity n+1. If an element x ∈ P.last.M has a decomposition dest x = ⟨a, f⟩ for some a ∈ P.A and f : P.last.B a → P.last.M, and f' is a path from x to α, then the destination of the assembled element ⟨x, f'⟩ equals the specialized destination applied to h and f': M.dest P ⟨x, f'⟩ = M.dest' P h f'.
Русский
Пусть P — многовариантная многоаргументная функторная полиномная структура. Пусть x ∈ P.last.M имеет разложение dest x = ⟨a, f⟩ для некоторого a ∈ P.A и f : P.last.B a → P.last.M, и пусть f' : M.Path P x ⟹ α. Тогда разрушение составленного элемента ⟨x, f'⟩ равно специализированному разрушению: M.dest P ⟨x, f'⟩ = M.dest' P h f'.
LaTeX
$$$\\forall {\\alpha : TypeVec\, n} \\ {x : P.last.M} \\ {a : P.A} \\ {f : P.last.B a \\to P.last.M} (h : PFunctor.M.dest x = ⟨a, f⟩) (f' : M.Path P x \\Rightarrow \\alpha), \\\\ M.dest P \\langle x, f' \\rangle = M.dest' P h f' $$$
Lean4
theorem dest_eq_dest' {α : TypeVec n} {x : P.last.M} {a : P.A} {f : P.last.B a → P.last.M}
(h : PFunctor.M.dest x = ⟨a, f⟩) (f' : M.Path P x ⟹ α) : M.dest P ⟨x, f'⟩ = M.dest' P h f' :=
M.dest'_eq_dest' _ _ _ _
