Ещё задачка про типизированную лямбду

В импликационном фрагменте классической пропозициональной логики у нас нет никаких связок кроме импликационной стрелочки. Поэтому мы не можем записать закон двойного отрицания или закон исключённого третьего - у нас для этого нет соответствующей связки. Однако имеется закон Пирса ((α → β) → α) → α, который в классической логике полностью эквивалентен упомянутым законам.

В просто типизированной лямбде тип ((α → β) → α) → α необитаем, поскольку соответствие Карри-Говарда задаёт изоморфизм с интуиционистской логикой, которая отличается от классической как раз отсутствием всех этих законов. Однако имеется слабый закон Пирса ((((α → β) → α) → α) → β) → β, про который известно, что он верен интуиционистски, а значит может быть получен конструктивно.

Откуда возникает задача: написать в просто типизированном лямбда-исчислении замкнутый терм типа ((((α → β) → α) → α) → β) → β.

Комменты не скринятся; Coq-читерам предлагается забыть про тактику auto и вспомнить про intros, apply и exact :)