∀ {L : FirstOrder.Language} {α : Type u'} {motive : {n : ℕ} → (a : L.BoundedFormula α n) → a.IsPrenex → Prop}
  {motive_1 :
    {n : ℕ} →
      {a : L.BoundedFormula α n} → (t : a.IsPrenex) → FirstOrder.Language.BoundedFormula.IsPrenex.below t → Prop},
  (∀ {n : ℕ} {φ : L.BoundedFormula α n} (h : φ.IsQF), motive_1 ⋯ ⋯) →
    (∀ {n : ℕ} {φ : L.BoundedFormula α (n + 1)} (h : φ.IsPrenex)
        (ih : FirstOrder.Language.BoundedFormula.IsPrenex.below h) (h_ih : motive φ h), motive_1 h ih → motive_1 ⋯ ⋯) →
      (∀ {n : ℕ} {φ : L.BoundedFormula α (n + 1)} (h : φ.IsPrenex)
          (ih : FirstOrder.Language.BoundedFormula.IsPrenex.below h) (h_ih : motive φ h),
          motive_1 h ih → motive_1 ⋯ ⋯) →
        ∀ {n : ℕ} {a : L.BoundedFormula α n} {t : a.IsPrenex}
          (t_1 : FirstOrder.Language.BoundedFormula.IsPrenex.below t), motive_1 t t_1