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