English
A simp-friendly specialization of the previous lemma: restrictingLeft with inclusion h gives the same realization after composing with the subtype projection.
Русский
Упрощённый частный случай: ограничение слева через включение h сохраняет реализацию после композиции с проекцией подпредставления.
LaTeX
$$$ (t.restrictVarLeft (Set.inclusion h)).realize (Sum.elim (v \circ (\uparrow)) xs) = t.realize (Sum.elim v xs) $$$
Lean4
/-- A special case of `realize_restrictVarLeft`, included because we can add the `simp` attribute
to it -/
@[simp]
theorem realize_restrictVarLeft' [DecidableEq α] {γ : Type*} {t : L.Term (α ⊕ γ)} {s : Set α} (h : ↑t.varFinsetLeft ⊆ s)
{v : α → M} {xs : γ → M} :
(t.restrictVarLeft (Set.inclusion h)).realize (Sum.elim (v ∘ (↑)) xs) = t.realize (Sum.elim v xs) :=
realize_restrictVarLeft _ (by simp)
