{L : FirstOrder.Language} →
  {α : Type u'} →
    {motive : (a : ℕ) → L.BoundedFormula α a → Sort u_1} →
      {a : ℕ} →
        (t : L.BoundedFormula α a) →
          ({n : ℕ} → motive n FirstOrder.Language.BoundedFormula.falsum) →
            ({n : ℕ} → (t₁ t₂ : L.Term (α ⊕ Fin n)) → motive n (FirstOrder.Language.BoundedFormula.equal t₁ t₂)) →
              ({n l : ℕ} →
                  (R : L.Relations l) →
                    (ts : Fin l → L.Term (α ⊕ Fin n)) → motive n (FirstOrder.Language.BoundedFormula.rel R ts)) →
                ({n : ℕ} → (f₁ f₂ : L.BoundedFormula α n) → motive n (f₁.imp f₂)) →
                  ({n : ℕ} → (f : L.BoundedFormula α (n + 1)) → motive n f.all) → motive a t