DEFINITION flt_wf_ind()
TYPE =
       ∀P:C→T→Prop
         .(∀c2:C.∀t2:T.(∀c1:C.∀t1:T.(flt c1 t1 c2 t2)→(P c1 t1))→(P c2 t2))→∀c:C.∀t:T.(P c t)
BODY =
Show proof