English
In a language with constants turned into variables, the realization of a term t.constantsToVars under a valuation that mirrors constants by their actual elements equals the realization of t under the valuation v.
Русский
В языке, где константы превращены в переменные, реализация t.constantsToVars под оценкой, отражающей константы их реальными элементами, равна реализации t под оценкой v.
LaTeX
$$$ t.constantsToVars.realize (Sum.elim (fun a => ↑(L.con a)) v) = t.realize v $$$
Lean4
@[simp]
theorem realize_constantsToVars [L[[α]].Structure M] [(lhomWithConstants L α).IsExpansionOn M] {t : L[[α]].Term β}
{v : β → M} : t.constantsToVars.realize (Sum.elim (fun a => ↑(L.con a)) v) = t.realize v := by
induction t with
| var => simp
| @func n f ts ih =>
cases n
· cases f
· simp only [realize, ih, constantsOn, constantsOnFunc, constantsToVars]
-- Porting note: below lemma does not work with simp for some reason
rw [withConstants_funMap_sumInl]
· simp only [realize, constantsToVars, Sum.elim_inl, funMap_eq_coe_constants]
rfl
· obtain - | f := f
· simp only [realize, ih, constantsOn, constantsOnFunc, constantsToVars]
-- Porting note: below lemma does not work with simp for some reason
rw [withConstants_funMap_sumInl]
· exact isEmptyElim f
