Объединение высшего порядка

Я работаю над средством доказательства теорем более высокого порядка, объединение которого, похоже, является самой сложной подзадачей.

Если алгоритм Уэта все еще считается современным, есть ли у кого-нибудь ссылки на его объяснения, написанные для понимания программистом, а не математиком?

Или даже какие-нибудь примеры, где это работает, а обычный алгоритм первого порядка - нет?