∀ {L : FirstOrder.Language} {α : Type u'} {k m n : ℕ} (km : k ≤ m) (mn : m ≤ n) (φ : L.BoundedFormula α k),
  FirstOrder.Language.BoundedFormula.castLE mn (FirstOrder.Language.BoundedFormula.castLE km φ) =
    FirstOrder.Language.BoundedFormula.castLE ⋯ φ