English
In the with-constants extension, the realization of t.varsToConstants under a valuation related to constants via the constant map equals the direct realization of t under v.
Русский
В расширении с константами реализация t.varsToConstants при оценке, связанной через константную карту, равна прямой реализации t при v.
LaTeX
$$$ t.varsToConstants.realize v (Sum.elim (fun a => L.constantMap (L.con a)) v) = t.realize v $$$
Lean4
@[simp]
theorem realize_varsToConstants [L[[α]].Structure M] [(lhomWithConstants L α).IsExpansionOn M] {t : L.Term (α ⊕ β)}
{v : β → M} : t.varsToConstants.realize v = t.realize (Sum.elim (fun a => ↑(L.con a)) v) := by
induction t with
| var ab => rcases ab with a | b <;> simp [Language.con]
| func f ts
ih =>
simp only [realize, constantsOn, constantsOnFunc, ih, varsToConstants]
-- Porting note: below lemma does not work with simp for some reason
rw [withConstants_funMap_sumInl]
