DEFINITION tlt_wf_ind()
TYPE =
       ∀P:T→Prop.(∀t:T.(∀v:T.(tlt v t)→(P v))→(P t))→∀t:T.(P t)
BODY =
Show proof