constantsVarsEquivLeft_symm_apply

English

Applying the left-variant of the constants-variables equivalence to a term matches the expected relabeling result.

Русский

Применение левой варианта эквивалентности константы-переменные к терму совпадает с ожидаемой переименовкой.

LaTeX

$$$\\mathrm{constantsVarsEquivLeft}(t) = t'$$$

Lean4

@[simp]
theorem constantsVarsEquivLeft_symm_apply (t : L.Term ((γ ⊕ α) ⊕ β)) :
    constantsVarsEquivLeft.symm t = varsToConstants (t.relabel (Equiv.sumAssoc _ _ _)) :=
  rfl

Похожие утверждения