DEFINITION sns3_lifts1()
TYPE =
       ∀e:C.∀hds:PList.∀c:C.(drop1 hds c e)→∀ts:TList.(sns3 e ts)→(sns3 c (lifts1 hds ts))
BODY =
Show proof