DEFINITION tlt_trans()
TYPE =
       ∀v:T.∀u:T.∀t:T.(tlt u v)→(tlt v t)→(tlt u t)
BODY =
        assume v: T
        assume u: T
        assume t: T
          we must prove (tlt u v)→(tlt v t)→(tlt u t)
          or equivalently (lt (weight u) (weight v))→(tlt v t)→(tlt u t)
          suppose H: lt (weight u) (weight v)
             we must prove (tlt v t)→(tlt u t)
             or equivalently (lt (weight v) (weight t))→(tlt u t)
             suppose H0: lt (weight v) (weight t)
                by (lt_trans . . . H H0)
                we proved lt (weight u) (weight t)
                that is equivalent to tlt u t
             we proved (lt (weight v) (weight t))→(tlt u t)
             that is equivalent to (tlt v t)→(tlt u t)
          we proved (lt (weight u) (weight v))→(tlt v t)→(tlt u t)
          that is equivalent to (tlt u v)→(tlt v t)→(tlt u t)
       we proved ∀v:T.∀u:T.∀t:T.(tlt u v)→(tlt v t)→(tlt u t)