∀ {L : FirstOrder.Language} {α : Type u'} {n : ℕ} {motive : (a : L.BoundedFormula α n) → a.IsQF → Prop}
  {motive_1 : {a : L.BoundedFormula α n} → (t : a.IsQF) → FirstOrder.Language.BoundedFormula.IsQF.below t → Prop},
  motive_1 ⋯ ⋯ →
    (∀ {φ : L.BoundedFormula α n} (h : φ.IsAtomic), motive_1 ⋯ ⋯) →
      (∀ {φ₁ φ₂ : L.BoundedFormula α n} (h₁ : φ₁.IsQF) (h₂ : φ₂.IsQF)
          (ih : FirstOrder.Language.BoundedFormula.IsQF.below h₁) (h₁_ih : motive φ₁ h₁)
          (ih_1 : FirstOrder.Language.BoundedFormula.IsQF.below h₂) (h₂_ih : motive φ₂ h₂),
          motive_1 h₁ ih → motive_1 h₂ ih_1 → motive_1 ⋯ ⋯) →
        ∀ {a : L.BoundedFormula α n} {t : a.IsQF} (t_1 : FirstOrder.Language.BoundedFormula.IsQF.below t),
          motive_1 t t_1