{R : Type u} →
  [inst : CommRing R] →
    {motive : RootPairingCat R → Sort u_1} →
      ((weight : Type v) →
          [weightIsAddCommGroup : AddCommGroup weight] →
            [weightIsModule : Module R weight] →
              (coweight : Type v) →
                [coweightIsAddCommGroup : AddCommGroup coweight] →
                  [coweightIsModule : Module R coweight] →
                    (index : Type v) →
                      (pairing : RootPairing index R weight coweight) →
                        motive
                          { weight := weight, weightIsAddCommGroup := weightIsAddCommGroup,
                            weightIsModule := weightIsModule, coweight := coweight,
                            coweightIsAddCommGroup := coweightIsAddCommGroup, coweightIsModule := coweightIsModule,
                            index := index, pairing := pairing }) →
        (t : RootPairingCat R) → motive t