DEFINITION cle()
TYPE =
       C→C→Prop
BODY =
λc1:C.λc2:C.le (cweight c1) (cweight c2)