English
If you have equivalences of terms and relations, you obtain an equivalence of bounded formulas by transporting along these equivalences.
Русский
Если имеются эквивалентности термов и отношений, то можно получить эквиваленто ограниченных формул, транспортируя через эти эквивалентности.
LaTeX
$$$\forall ft fr,\; (ft : n \mapsto L.Term) \text{ and } (fr : n \mapsto L.Relations n)\; \Rightarrow\; (L.BoundedFormula α n) \simeq (L'.BoundedFormula β n)$ via mapTermRelEquiv.$$
Lean4
/-- Raises all of the bound variables of a formula greater than or equal to `m` by `n'`. -/
def liftAt : ∀ {n : ℕ} (n' _m : ℕ), L.BoundedFormula α n → L.BoundedFormula α (n + n') := fun {_} n' m φ =>
φ.mapTermRel (fun _ t => t.liftAt n' m) (fun _ => id) fun _ => castLE (by rw [add_assoc, add_comm 1, add_assoc])
