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