DEFINITION llt_head_dx()
TYPE =
       ∀a1:A.∀a2:A.(llt a2 (AHead a1 a2))
BODY =
        assume a1: A
        assume a2: A
          by (le_plus_r . .)
          we proved le (lweight a2) (plus (lweight a1) (lweight a2))
          by (le_n_S . . previous)
          we proved le (S (lweight a2)) (S (plus (lweight a1) (lweight a2)))
          that is equivalent to llt a2 (AHead a1 a2)
       we proved ∀a1:A.∀a2:A.(llt a2 (AHead a1 a2))