{R : Type u} →
  [inst : Ring R] →
    {motive : ModuleCat R → Sort u_1} →
      ((carrier : Type v) →
          [isAddCommGroup : AddCommGroup carrier] →
            [isModule : Module R carrier] →
              motive { carrier := carrier, isAddCommGroup := isAddCommGroup, isModule := isModule }) →
        (t : ModuleCat R) → motive t