the other direction of hlist_app_assoc.

- they aren't proved simultaneously because of the cast