Relabeling in model theory

Stream: mathlib4

[Uni Marx]

I'm trying to implement relativizations of formulas for a personal project and this is the definition I'm using so far:

import ModelTheory.Syntax
namespace FirstOrder.Language

open FirstOrder.Language
open FirstOrder
open Language Structure
variable {L : Language} {n : ℕ}
variable (χ : L.BoundedFormula α 1)

namespace BoundedFormula
def relativize : {n : ℕ} → L.BoundedFormula α n → L.BoundedFormula α n
| _, falsum => falsum
| _, imp φ ψ => imp (relativize φ) (relativize ψ)
| _, rel r xs => rel r xs
| _, equal a b => equal a b
| n, all φ => all (cast (congrArg _ (add_comm 1 n)) (χ.liftAt n 0) ⟹ (relativize φ))
end BoundedFormula
lemma relativize_all_aux {φ : L.BoundedFormula α (n + 1)} (f : _) (k : _):
  BoundedFormula.Realize (M := R)  (all (cast (congrArg _ (add_comm 1 n)) (χ.liftAt n 0) ⟹ φ)) f k
    ↔ (∀ x, BoundedFormula.Realize (M := R) χ f (λ _ ↦ x) → BoundedFormula.Realize (M := R) φ f (Fin.snoc k x)) := by sorry

The cast makes it pretty much unusable though, does anyone who has more knowledge of that part of the library have any idea how to approach it? None of the cast-like functions (not even BoundedFormula.subst and the like) seem to be able to "push the variable 0 to the maximum"