I feel sorry for whoever has to read and understand the solution. It looks like the typical convoluted unreadable mess I see the models generate for software. It might be technically correct, but gaining insight from it is just intellectual hell.
Extra credits if it is proven that the proof cannot be reduced any further.
https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspon...