{R : Type u_1} →
  [inst : CommRing R] →
    {I : Ideal R} →
      {motive : HenselianRing R I → Sort u} →
        (t : HenselianRing R I) →
          ((jac : I ≤ ⊥.jacobson) →
              (is_henselian :
                  ∀ (f : Polynomial R),
                    f.Monic →
                      ∀ (a₀ : R),
                        Polynomial.eval a₀ f ∈ I →
                          IsUnit ((Ideal.Quotient.mk I) (Polynomial.eval a₀ (Polynomial.derivative f))) →
                            ∃ a, f.IsRoot a ∧ a - a₀ ∈ I) →
                motive ⋯) →
            motive t