functor
(
X
:
S
)
->
HI