DEFINITION fweight()
TYPE =
C
→
T
→
nat
BODY =
λ
c:
C
.
λ
t:
T
.
plus
(
cweight
c) (
tweight
t)