DEFINITION flt_shift()
TYPE =
       ∀k:K.∀c:C.∀u:T.∀t:T.(flt (CHead c k u) t c (THead k u t))
BODY =
Show proof