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