English
Let g be a function from the set of free variables to a sum type β ⊕ Fin(n), and let φ be a bounded formula with k+1 variables. Relabeling all bound occurrences inside φ by g commutes with relabeling the formula itself: φ.all.relabel g = (φ.relabel g).all.
Русский
Пусть g: α → β ⊕ Fin(n) и φ — ограниченная формула с k+1 переменной. Переименование всех связанных переменных внутри φ по g коммутирует с переименованием самой формулы: φ.all.relabel g = (φ.relabel g).all.
LaTeX
$$$\\forall g:\\alpha \\to (\\beta \\oplus \\mathrm{Fin}(n))\\,\\forall k\\in\\mathbb{N}\\,\\forall \\phi:\\,L.BoundedFormula\\,\\alpha\\,(k+1):\\; \\phi.\\text{all}.\\mathrm{relabel}\\, g = (\\phi.\\mathrm{relabel}\\, g).\\text{all}$$$
Lean4
@[simp]
theorem relabel_all (g : α → β ⊕ (Fin n)) {k} (φ : L.BoundedFormula α (k + 1)) : φ.all.relabel g = (φ.relabel g).all :=
by
rw [relabel, mapTermRel, relabel]
simp
