Sort u →
  {Γ : Type u_1} →
    [inst : LinearOrderedCommGroupWithZero Γ] →
      {A : Type u_2} →
        [inst_1 : Ring A] →
          {v : Valuation A Γ} →
            [hv : v.IsRankOneDiscrete] →
              v.Uniformizer →
                {Γ' : Type u_1} →
                  [inst' : LinearOrderedCommGroupWithZero Γ'] →
                    {A' : Type u_2} →
                      [inst'_1 : Ring A'] →
                        {v' : Valuation A' Γ'} → [hv' : v'.IsRankOneDiscrete] → v'.Uniformizer → Sort u