DEFINITION llt()
TYPE =
A
→
A
→
Prop
BODY =
Show proof