{L : FirstOrder.Language} →
  {α : Type u_3} →
    (motive : (x : ℕ) → L.BoundedFormula α x → L.BoundedFormula α x → Sort u_4) →
      (x : ℕ) →
        (x_1 x_2 : L.BoundedFormula α x) →
          ((n : ℕ) →
              (φ : L.BoundedFormula α n) →
                (ψ : L.BoundedFormula α (n + 1)) →
                  motive n φ
                    ((ψ.imp FirstOrder.Language.BoundedFormula.falsum).all.imp
                      FirstOrder.Language.BoundedFormula.falsum)) →
            ((n : ℕ) → (φ : L.BoundedFormula α n) → (ψ : L.BoundedFormula α (n + 1)) → motive n φ ψ.all) →
              ((_n : ℕ) → (φ ψ : L.BoundedFormula α _n) → motive _n φ ψ) → motive x x_1 x_2