{R : Type u_2} →
  {motive : AddMonoidWithOne R → Sort u} →
    (t : AddMonoidWithOne R) →
      ([toNatCast : NatCast R] →
          [toAddMonoid : AddMonoid R] →
            [toOne : One R] →
              (natCast_zero : ↑0 = 0) →
                (natCast_succ : ∀ (n : ℕ), ↑(n + 1) = ↑n + 1) →
                  motive
                    { toNatCast := toNatCast, toAddMonoid := toAddMonoid, toOne := toOne, natCast_zero := natCast_zero,
                      natCast_succ := natCast_succ }) →
        motive t