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