DEFINITION sns3_lifts()
TYPE =
       ∀c:C
         .∀d:C
           .∀h:nat
             .∀i:nat.(drop h i c d)→∀ts:TList.(sns3 d ts)→(sns3 c (lifts h i ts))
BODY =
Show proof