type
h
1
'(
α
, α
2
) = τ
1
[
h
2
(
α
) ← α
2
]
type
h
2
(
α
) = τ
2
[
h
1
(
α
) ←
h
1
'(
α
,
h
2
(
α
))]
type
h
1
(
α
) =
h
1
'(
α
,
h
2
(
α
))