{L : FirstOrder.Language} →
  {M : Type u_5} →
    {α : Type u_3} →
      (motive : (x : ℕ) → L.BoundedFormula α x → (α → M) → (Fin x → M) → Sort u_4) →
        (x : ℕ) →
          (x_1 : L.BoundedFormula α x) →
            (x_2 : α → M) →
              (x_3 : Fin x → M) →
                ((x : ℕ) →
                    (_v : α → M) → (_xs : Fin x → M) → motive x FirstOrder.Language.BoundedFormula.falsum _v _xs) →
                  ((x : ℕ) →
                      (t₁ t₂ : L.Term (α ⊕ Fin x)) →
                        (v : α → M) →
                          (xs : Fin x → M) → motive x (FirstOrder.Language.BoundedFormula.equal t₁ t₂) v xs) →
                    ((x l : ℕ) →
                        (R : L.Relations l) →
                          (ts : Fin l → L.Term (α ⊕ Fin x)) →
                            (v : α → M) →
                              (xs : Fin x → M) → motive x (FirstOrder.Language.BoundedFormula.rel R ts) v xs) →
                      ((x : ℕ) →
                          (f₁ f₂ : L.BoundedFormula α x) → (v : α → M) → (xs : Fin x → M) → motive x (f₁.imp f₂) v xs) →
                        ((x : ℕ) →
                            (f : L.BoundedFormula α (x + 1)) → (v : α → M) → (xs : Fin x → M) → motive x f.all v xs) →
                          motive x x_1 x_2 x_3