This is awesome. I didn't even really see what was happening until it was too late. If you enjoyed that you might enjoy the structure of the proof of the compl

This is awesome. I didn't even really see what was happening until it was too late. If you enjoyed that you might enjoy the structure of the proof of the complexity of type inference for \-calculus: http://www.cs.brandeis.edu/~mairson/Papers/jfp02.pdf http://www.cs.brandeis.edu/~mairson/Papers/jfp02.pdf . They construct arbitrary boolean circuits from simple types and evaluate the circuits through type checking.