DEFINITION tlt_trans()
TYPE =
∀
v:
T
.
∀
u:
T
.
∀
t:
T
.(
tlt
u v)
→
(
tlt
v t)
→
(
tlt
u t)
BODY =
Show proof