DEFINITION llt_head_dx()
TYPE =
∀
a1:
A
.
∀
a2:
A
.(
llt
a2 (
AHead
a1 a2))
BODY =
Show proof