∀ {L : FirstOrder.Language} {α : Type u_3} (motive : (x : ℕ) → L.BoundedFormula α x → L.BoundedFormula α x → Sort u_4)
  (n : ℕ) (φ : L.BoundedFormula α n) (ψ : L.BoundedFormula α (n + 1))
  (h_1 :
    (n : ℕ) →
      (φ : L.BoundedFormula α n) →
        (ψ : L.BoundedFormula α (n + 1)) →
          motive n φ
            ((ψ.imp FirstOrder.Language.BoundedFormula.falsum).all.imp FirstOrder.Language.BoundedFormula.falsum))
  (h_2 : (n : ℕ) → (φ : L.BoundedFormula α n) → (ψ : L.BoundedFormula α (n + 1)) → motive n φ ψ.all)
  (h_3 : (_n : ℕ) → (φ ψ : L.BoundedFormula α _n) → motive _n φ ψ),
  (match n, φ, (ψ.imp FirstOrder.Language.BoundedFormula.falsum).all.imp FirstOrder.Language.BoundedFormula.falsum with
    | n, φ, (ψ.imp FirstOrder.Language.BoundedFormula.falsum).all.imp FirstOrder.Language.BoundedFormula.falsum =>
      h_1 n φ ψ
    | n, φ, ψ.all => h_2 n φ ψ
    | _n, φ, ψ => h_3 _n φ ψ) =
    h_1 n φ ψ