DEFINITION flt_trans()
TYPE =
       c1:C.c2:C.t1:T.t2:T.(flt c1 t1 c2 t2)c3:C.t3:T.(flt c2 t2 c3 t3)(flt c1 t1 c3 t3)
BODY =
Show proof