{P : Sort u} →
  {Γ : Type u_8} →
    {R : Type u_9} →
      {inst : PartialOrder Γ} →
        {inst_1 : AddCommMonoid R} →
          {α : Type u_7} →
            {t : HahnSeries.SummableFamily Γ R α} →
              {Γ' : Type u_8} →
                {R' : Type u_9} →
                  {inst' : PartialOrder Γ'} →
                    {inst'_1 : AddCommMonoid R'} →
                      {α' : Type u_7} →
                        {t' : HahnSeries.SummableFamily Γ' R' α'} →
                          Γ = Γ' →
                            R = R' →
                              inst ≍ inst' →
                                inst_1 ≍ inst'_1 → α = α' → t ≍ t' → HahnSeries.SummableFamily.noConfusionType P t t'