Code from book "Handbook of Practical Logic and Automated Reasoning" by John Harrison - View it on GitHub