DEFINITION sn3_gen_head()
TYPE =
       ∀k:K.∀c:C.∀u:T.∀t:T.(sn3 c (THead k u t))→(sn3 c u)
BODY =
Show proof