English
There is a way to restrict any term to a new set of variables when you only keep track of the left-hand variables that appear. Given a term t in variables α ⊕ γ and a map f from the left part of t to β, you obtain a new term in β ⊕ γ whose left variables are the image of t's left variables under f, and whose right variables are unchanged.
Русский
Существует способ ограничить любую термку новым набором переменных, сохранив только левые переменные из суммы. Пусть t — терм в переменных α ⊕ γ и dопустимая отображение f от левой части t в β; тогда получается новый терм в β ⊕ γ, чьи левые переменные являются образом переменных левой части t под f, а правые переменные не изменяются.
LaTeX
$$$\\forall t \\in L\\text{.Term}(\\alpha \\oplus \\gamma),\\ \\forall f:(t.varFinsetLeft\\to\\beta),\\ \\exists! t' \\in L\\text{.Term}(\\beta \\oplus \\gamma)\\; \\text{such that } t' \\text{ is obtained from } t \\text{ by renaming each left variable } a\\in \\alpha \\text{ to } f(a) \\text{ and leaving right variables unchanged.}$$$
Lean4
/-- Restricts a term to use only a set of the given variables on the left side of a sum. -/
def restrictVarLeft [DecidableEq α] {γ : Type*} : ∀ (t : L.Term (α ⊕ γ)) (_f : t.varFinsetLeft → β), L.Term (β ⊕ γ)
| var (Sum.inl a), f => var (Sum.inl (f ⟨a, mem_singleton_self a⟩))
| var (Sum.inr a), _f => var (Sum.inr a)
| func F ts, f =>
func F fun i =>
(ts i).restrictVarLeft (f ∘ Set.inclusion (subset_biUnion_of_mem (fun i => varFinsetLeft (ts i)) (mem_univ i)))
