1. Use pi-calculus to model the 2-dining philosopher problem.
2. Use SUM and STRUCT to prove the SUM2 Rule:
α