DEFINITION flt()
TYPE =
       C→T→C→T→Prop
BODY =
λc1:C.λt1:T.λc2:C.λt2:T.lt (fweight c1 t1) (fweight c2 t2)