DEFINITION lift1_flat()
TYPE =
       ∀f:F
         .∀hds:PList
           .∀u:T
             .∀t:T
               .eq
                 T
                 lift1 hds (THead (Flat f) u t)
                 THead (Flat f) (lift1 hds u) (lift1 hds t)
BODY =
Show proof