DEFINITION lifts1_flat()
TYPE =
       ∀f:F
         .∀hds:PList
           .∀t:T
             .∀ts:TList
               .eq
                 T
                 lift1 hds (THeads (Flat f) ts t)
                 THeads (Flat f) (lifts1 hds ts) (lift1 hds t)
BODY =
Show proof