English
There is a canonical map from terms that may contain constants to terms over an expanded language with extra variables, by relocating constants to the left part and leaving variables on the right intact.
Русский
Существует каноническая карта из термов с константами в термы над расширенным языком с дополнительными переменными, перемещая константы в левую часть и оставляя переменные справа без изменений.
LaTeX
$$$\\mathrm{constantsToVars}: L[[\\gamma]].Term(\\alpha) \\to L.Term(\\gamma\\oplus\\alpha)$, описанное по правилам: константы отправляются в левую часть, переменные остаются на месте, а операции применяются рекурсивно.$$
Lean4
/-- Sends a term with constants to a term with extra variables. -/
@[simp]
def constantsToVars : L[[γ]].Term α → L.Term (γ ⊕ α)
| var a => var (Sum.inr a)
| @func _ _ 0 f ts => Sum.casesOn f (fun f => func f fun i => (ts i).constantsToVars) fun c => var (Sum.inl c)
| @func _ _ (_n + 1) f ts => Sum.casesOn f (fun f => func f fun i => (ts i).constantsToVars) fun c => isEmptyElim c
