DEFINITION drop1_skip_bind()
TYPE =
       ∀b:B
         .∀e:C
           .∀hds:PList
             .∀c:C
               .∀u:T
                 .drop1 hds c e
                   →drop1 (Ss hds) (CHead c (Bind b) (lift1 hds u)) (CHead e (Bind b) u)
BODY =
Show proof