DEFINITION flt_arith0()
TYPE =
       ∀k:K.∀c:C.∀t:T.∀i:nat.(flt c t (CHead c k t) (TLRef i))
BODY =
Show proof