DEFINITION flt_trans()
TYPE =
       ∀c1:C.∀c2:C.∀t1:T.∀t2:T.(flt c1 t1 c2 t2)→∀c3:C.∀t3:T.(flt c2 t2 c3 t3)→(flt c1 t1 c3 t3)
BODY =
        assume c1: C
        assume c2: C
        assume t1: T
        assume t2: T
          we must prove (flt c1 t1 c2 t2)→∀c3:C.∀t3:T.(flt c2 t2 c3 t3)→(flt c1 t1 c3 t3)
          or equivalently (lt (fweight c1 t1) (fweight c2 t2))→∀c3:C.∀t3:T.(flt c2 t2 c3 t3)→(flt c1 t1 c3 t3)
           suppose H: lt (fweight c1 t1) (fweight c2 t2)
           assume c3: C
           assume t3: T
             we must prove (flt c2 t2 c3 t3)→(flt c1 t1 c3 t3)
             or equivalently (lt (fweight c2 t2) (fweight c3 t3))→(flt c1 t1 c3 t3)
             suppose H0: lt (fweight c2 t2) (fweight c3 t3)
                by (lt_trans . . . H H0)
                we proved lt (fweight c1 t1) (fweight c3 t3)
                that is equivalent to flt c1 t1 c3 t3
             we proved (lt (fweight c2 t2) (fweight c3 t3))→(flt c1 t1 c3 t3)
             that is equivalent to (flt c2 t2 c3 t3)→(flt c1 t1 c3 t3)
          we proved (lt (fweight c1 t1) (fweight c2 t2))→∀c3:C.∀t3:T.(flt c2 t2 c3 t3)→(flt c1 t1 c3 t3)
          that is equivalent to (flt c1 t1 c2 t2)→∀c3:C.∀t3:T.(flt c2 t2 c3 t3)→(flt c1 t1 c3 t3)
       we proved ∀c1:C.∀c2:C.∀t1:T.∀t2:T.(flt c1 t1 c2 t2)→∀c3:C.∀t3:T.(flt c2 t2 c3 t3)→(flt c1 t1 c3 t3)