∀ {L : FirstOrder.Language} {L' : FirstOrder.Language} {α : Type u'} (g : L →ᴸ L') (x : ℕ)
  (f₁ f₂ : L.BoundedFormula α x), g.onBoundedFormula (f₁.imp f₂) = (g.onBoundedFormula f₁).imp (g.onBoundedFormula f₂)