{A : Type u_1} →
  {B : Type u_2} →
    [inst : CommRing A] →
      [inst_1 : CommRing B] →
        [inst_2 : Algebra A B] →
          [inst_3 : Differential B] →
            {motive : Differential.ContainConstants A B → Sort u} →
              ((mem_range_of_deriv_eq_zero : ∀ {x : B}, x′ = 0 → x ∈ (algebraMap A B).range) → motive ⋯) →
                (t : Differential.ContainConstants A B) → motive t