English
For a term t of Sum α γ, restricting the left variables via f and relabeling the right side by xs' yields realization equal to applying t.realize to Sum.elim xs' xs.
Русский
Для терма t типа Sum α γ, ограничение левых переменных через f и переименование правой части xs' дают ту же реализацию, что и применение t.realize к Sum.elim xs' xs.
LaTeX
$$$ (t.restrictVarLeft f).realize xs = t.realize (Sum.elim xs' (xs \circ Sum.inr)) $$$
Lean4
theorem realize_restrictVarLeft [DecidableEq α] {γ : Type*} {t : L.Term (α ⊕ γ)} {f : t.varFinsetLeft → β}
{xs : β ⊕ γ → M} (xs' : α → M) (hxs' : ∀ a, xs (Sum.inl (f a)) = xs' a) :
(t.restrictVarLeft f).realize xs = t.realize (Sum.elim xs' (xs ∘ Sum.inr)) := by
induction t with
| var a => cases a <;> simp [restrictVarLeft, hxs']
| func _ _ ih => exact congr rfl (funext fun i => ih i (by simp [hxs']))
