{P : Sort u} →
  {Γ : Type u_1} →
    {R : Type u_2} →
      {inst : PartialOrder Γ} →
        {inst_1 : Zero R} →
          {t : HahnSeries Γ R} →
            {Γ' : Type u_1} →
              {R' : Type u_2} →
                {inst' : PartialOrder Γ'} →
                  {inst'_1 : Zero R'} →
                    {t' : HahnSeries Γ' R'} →
                      Γ = Γ' → R = R' → inst ≍ inst' → inst_1 ≍ inst'_1 → t ≍ t' → HahnSeries.noConfusionType P t t'