{P : Sort u} →
  {α : Type u_1} →
    {inst : DecidableEq α} →
      {inst_1 : Fintype α} →
        {g : Equiv.Perm α} →
          {t : g.Basis} →
            {α' : Type u_1} →
              {inst' : DecidableEq α'} →
                {inst'_1 : Fintype α'} →
                  {g' : Equiv.Perm α'} →
                    {t' : g'.Basis} →
                      α = α' →
                        inst ≍ inst' → inst_1 ≍ inst'_1 → g ≍ g' → t ≍ t' → Equiv.Perm.Basis.noConfusionType P t t'