DEFINITION lweight_repl()
TYPE =
       ∀g:G.∀a1:A.∀a2:A.(leq g a1 a2)→(eq nat (lweight a1) (lweight a2))
BODY =
Show proof