DEFINITION getl_gen_S()
TYPE =
       ∀k:K
         .∀c:C.∀x:C.∀u:T.∀h:nat.(getl (S h) (CHead c k u) x)→(getl (r k h) c x)
BODY =
Show proof