{R : Type u_1} →
  [inst : CommSemiring R] →
    {P : Ideal R → Prop} →
      {motive : Ideal.IsOka P → Sort u} →
        (t : Ideal.IsOka P) →
          ((top : P ⊤) →
              (oka : ∀ {I : Ideal R} {a : R}, P (I ⊔ Ideal.span {a}) → P (Submodule.colon I ↑(Ideal.span {a})) → P I) →
                motive ⋯) →
            motive t