{P : Sort u_1} →
  {G : Type u} →
    {inst : Group G} →
      {t : GroupFilterBasis G} →
        {G' : Type u} →
          {inst' : Group G'} →
            {t' : GroupFilterBasis G'} → G = G' → inst ≍ inst' → t ≍ t' → GroupFilterBasis.noConfusionType P t t'