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