DEFINITION iso_gen_head()
TYPE =
       ∀k:K.∀v1:T.∀t1:T.∀u2:T.(iso (THead k v1 t1) u2)→(ex_2 T T λv2:T.λt2:T.eq T u2 (THead k v2 t2))
BODY =
Show proof