{P : Sort u} →
  {M : Type u_1} →
    {inst : Group M} →
      {α : Type u_2} →
        {inst_1 : MulAction M α} →
          {t : MulAction.IwasawaStructure M α} →
            {M' : Type u_1} →
              {inst' : Group M'} →
                {α' : Type u_2} →
                  {inst'_1 : MulAction M' α'} →
                    {t' : MulAction.IwasawaStructure M' α'} →
                      M = M' →
                        inst ≍ inst' →
                          α = α' → inst_1 ≍ inst'_1 → t ≍ t' → MulAction.IwasawaStructure.noConfusionType P t t'