{P : Sort u} →
  {β : Type u_1} →
    {G : Type u_2} →
      {α : Type u_3} →
        {inst : Monoid G} →
          {inst_1 : AddMonoid α} →
            {t : SlashAction β G α} →
              {β' : Type u_1} →
                {G' : Type u_2} →
                  {α' : Type u_3} →
                    {inst' : Monoid G'} →
                      {inst'_1 : AddMonoid α'} →
                        {t' : SlashAction β' G' α'} →
                          β = β' →
                            G = G' →
                              α = α' → inst ≍ inst' → inst_1 ≍ inst'_1 → t ≍ t' → SlashAction.noConfusionType P t t'