∀ {R : Type u_1} {Γ₀ : Type u_2} [inst : Ring R] [inst_1 : LinearOrderedCommMonoidWithZero Γ₀] (f g : Valuation R Γ₀),
  (fun f => (↑f.toMonoidWithZeroHom).toFun) f = (fun f => (↑f.toMonoidWithZeroHom).toFun) g → f = g