…And it comes to be that the soothing light at the end of your tunnel is just a freight train coming your way…
8. FORMAL PROOF II------------------let phi = p(x)1. phi => Ax.phi UG2. (phi => Ax.phi) => Ax.(phi => Ax. phi) UG 13. Ax.(phi => Ax. phi) MP 1,24. Ax.phi => Ax.Ax.phi UD 35. Ax.phi => Ax.phi [x6. Ax.phi => phi[x7. Ax.p(x) => p(y) write phi as p(x)8. Ax.p(x) => Ay.p(y) UG 7 Voodoo.

