DEFINITION llt_trans()
TYPE =
∀
a1:
A
.
∀
a2:
A
.
∀
a3:
A
.(
llt
a1 a2)
→
(
llt
a2 a3)
→
(
llt
a1 a3)
BODY =
Show proof