DEFINITION flt()
TYPE =
       C→T→C→T→Prop
BODY =
Show proof