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