DEFINITION tweight_lt()
TYPE =
       ∀t:T.(lt O (tweight t))
BODY =
Show proof