∀ {L : FirstOrder.Language} {L' : FirstOrder.Language} {α : Type u'} {β : Type v'} {γ : Type u_1}
  {L'' : FirstOrder.Language} (ft : (n : ℕ) → L.Term (α ⊕ Fin n) → L'.Term (β ⊕ Fin n))
  (fr : (n : ℕ) → L.Relations n → L'.Relations n) (ft' : (n : ℕ) → L'.Term (β ⊕ Fin n) → L''.Term (γ ⊕ Fin n))
  (fr' : (n : ℕ) → L'.Relations n → L''.Relations n) {n : ℕ} (φ : L.BoundedFormula α n),
  FirstOrder.Language.BoundedFormula.mapTermRel ft' fr' (fun x => id)
      (FirstOrder.Language.BoundedFormula.mapTermRel ft fr (fun x => id) φ) =
    FirstOrder.Language.BoundedFormula.mapTermRel (fun x => ft' x ∘ ft x) (fun x => fr' x ∘ fr x) (fun x => id) φ