∀ {L : FirstOrder.Language} {L' : FirstOrder.Language} {α : Type u'} {β : Type v'} {g : ℕ → ℕ}
  (ft : (n : ℕ) → L.Term (α ⊕ Fin n) → L'.Term (β ⊕ Fin (g n))) (fr : (n : ℕ) → L.Relations n → L'.Relations n)
  (h : (n : ℕ) → L'.BoundedFormula β (g (n + 1)) → L'.BoundedFormula β (g n + 1)) (x : ℕ) (x_1 : L.BoundedFormula α x),
  FirstOrder.Language.BoundedFormula.mapTermRel ft fr h x_1 =
    match x, x_1 with
    | _n, FirstOrder.Language.BoundedFormula.falsum => FirstOrder.Language.BoundedFormula.falsum
    | _n, FirstOrder.Language.BoundedFormula.equal t₁ t₂ =>
      FirstOrder.Language.BoundedFormula.equal (ft _n t₁) (ft _n t₂)
    | _n, FirstOrder.Language.BoundedFormula.rel R ts =>
      FirstOrder.Language.BoundedFormula.rel (fr l R) fun i => ft _n (ts i)
    | _n, φ₁.imp φ₂ =>
      (FirstOrder.Language.BoundedFormula.mapTermRel ft fr h φ₁).imp
        (FirstOrder.Language.BoundedFormula.mapTermRel ft fr h φ₂)
    | n, φ.all => (h n (FirstOrder.Language.BoundedFormula.mapTermRel ft fr h φ)).all