∀ {L : FirstOrder.Language} {L' : FirstOrder.Language} {α : Type u'} (φ : L →ᴸ L') (l : ℕ) (_f : L.Functions l)
  (ts : Fin l → L.Term α),
  φ.onTerm (FirstOrder.Language.func _f ts) = FirstOrder.Language.func (φ.onFunction _f) fun i => φ.onTerm (ts i)