DEFINITION sn3_gen_lift()
TYPE =
       ∀c1:C.∀t:T.∀h:nat.∀d:nat.(sn3 c1 (lift h d t))→∀c2:C.(drop h d c1 c2)→(sn3 c2 t)
BODY =
Show proof