{R : Type u_1} →
  [inst : CommMonoid R] →
    {R' : Type u_2} →
      [inst_1 : CommMonoidWithZero R'] →
        {motive : MulChar R R' → Sort u} →
          (t : MulChar R R') →
            ((toMonoidHom : R →* R') →
                (map_nonunit' : ∀ (a : R), ¬IsUnit a → (↑toMonoidHom).toFun a = 0) →
                  motive { toMonoidHom := toMonoidHom, map_nonunit' := map_nonunit' }) →
              motive t