DEFINITION sn3_lift()
TYPE =
       ∀d:C.∀t:T.(sn3 d t)→∀c:C.∀h:nat.∀i:nat.(drop h i c d)→(sn3 c (lift h i t))
BODY =
Show proof