{P : Sort u} →
  {R : Type u_1} →
    {inst : Ring R} →
      {Γ₀ : Type u_2} →
        {inst_1 : LinearOrderedCommGroupWithZero Γ₀} →
          {v : Valuation R Γ₀} →
            {t : v.RankOne} →
              {R' : Type u_1} →
                {inst' : Ring R'} →
                  {Γ₀' : Type u_2} →
                    {inst'_1 : LinearOrderedCommGroupWithZero Γ₀'} →
                      {v' : Valuation R' Γ₀'} →
                        {t' : v'.RankOne} →
                          R = R' →
                            inst ≍ inst' →
                              Γ₀ = Γ₀' → inst_1 ≍ inst'_1 → v ≍ v' → t ≍ t' → Valuation.RankOne.noConfusionType P t t'