∀ {L : FirstOrder.Language} {α : Type u_3} (motive : (x x_1 : ℕ) → x ≤ x_1 → L.BoundedFormula α x → Sort u_4)
  (_m _n : ℕ) (h : _m ≤ _n) (f : L.BoundedFormula α (_m + 1))
  (h_1 : (_m _n : ℕ) → (_h : _m ≤ _n) → motive _m _n _h FirstOrder.Language.BoundedFormula.falsum)
  (h_2 :
    (_m _n : ℕ) →
      (h : _m ≤ _n) → (t₁ t₂ : L.Term (α ⊕ Fin _m)) → motive _m _n h (FirstOrder.Language.BoundedFormula.equal t₁ t₂))
  (h_3 :
    (_m _n : ℕ) →
      (h : _m ≤ _n) →
        (l : ℕ) →
          (R : L.Relations l) →
            (ts : Fin l → L.Term (α ⊕ Fin _m)) → motive _m _n h (FirstOrder.Language.BoundedFormula.rel R ts))
  (h_4 : (_m _n : ℕ) → (h : _m ≤ _n) → (f₁ f₂ : L.BoundedFormula α _m) → motive _m _n h (f₁.imp f₂))
  (h_5 : (_m _n : ℕ) → (h : _m ≤ _n) → (f : L.BoundedFormula α (_m + 1)) → motive _m _n h f.all),
  (match _m, _n, h, f.all with
    | _m, _n, _h, FirstOrder.Language.BoundedFormula.falsum => h_1 _m _n _h
    | _m, _n, h, FirstOrder.Language.BoundedFormula.equal t₁ t₂ => h_2 _m _n h t₁ t₂
    | _m, _n, h, FirstOrder.Language.BoundedFormula.rel R ts => h_3 _m _n h l R ts
    | _m, _n, h, f₁.imp f₂ => h_4 _m _n h f₁ f₂
    | _m, _n, h, f.all => h_5 _m _n h f) =
    h_5 _m _n h f