DEFINITION llt_wf_ind()
TYPE =
       ∀P:A→Prop.(∀a2:A.(∀a1:A.(llt a1 a2)→(P a1))→(P a2))→∀a:A.(P a)
BODY =
Show proof