DEFINITION wf3_gen_head2()
TYPE =
       ∀g:G.∀x:C.∀c:C.∀v:T.∀k:K.(wf3 g x (CHead c k v))→(ex B λb:B.eq K k (Bind b))
BODY =
Show proof