DEFINITION clt()
TYPE =
C
→
C
→
Prop
BODY =
λ
c1:
C
.
λ
c2:
C
.
lt
(
cweight
c1) (
cweight
c2)