English
For any bounded formula φ, relabeling by Sum.inl maps φ to the same formula as casting via the left injection to accommodate the new bound index: φ.relabel Sum.inl = φ.castLE (ge_of_eq (zero_add n)).
Русский
Для любой ограниченной формулы φ переразметка Sum.inl эквивалентна приведению к новому диапазону, получаемому через левое внедрение: φ.relabel Sum.inl = φ.castLE (ge_of_eq (zero_add n)).
LaTeX
$$$\\forall \\phi:\\,L.BoundedFormula\\,\\alpha\\,n:\\; (\\phi.\\relabel\\mathrm{Sum.inl}) = \\phi.castLE(\\mathrm{ge\\_of\\_eq}(\\mathrm{zero\\_add}\\, n))$$$
Lean4
@[simp]
theorem relabel_sumInl (φ : L.BoundedFormula α n) :
(φ.relabel Sum.inl : L.BoundedFormula α (0 + n)) = φ.castLE (ge_of_eq (zero_add n)) :=
by
simp only [relabel, relabelAux_sumInl]
induction φ with
| falsum => rfl
| equal => simp [Fin.natAdd_zero, castLE_of_eq, mapTermRel]
| rel => simp [Fin.natAdd_zero, castLE_of_eq, mapTermRel]; rfl
| imp _ _ ih1 ih2 => simp_all [mapTermRel]
| all _ ih3 => simp_all [mapTermRel]
