DEFINITION flt_arith1()
TYPE =
       ∀k1:K.∀c1:C.∀c2:C.∀t1:T.(cle (CHead c1 k1 t1) c2)→∀k2:K.∀t2:T.∀i:nat.(flt c1 t1 (CHead c2 k2 t2) (TLRef i))
BODY =
Show proof