DEFINITION lift1_bind()
TYPE =
       ∀b:B
         .∀hds:PList
           .∀u:T
             .∀t:T
               .eq
                 T
                 lift1 hds (THead (Bind b) u t)
                 THead (Bind b) (lift1 hds u) (lift1 (Ss hds) t)
BODY =
Show proof