added refinement of result in application of pure functions to impure arguments; killed a couple of TODOs in millionaires; fixed some syntax issues in z3.fs ... bootstraps again