Remove the dependency on the compiler from impl_proofs

For now, the compiler is broken, and I want to work on
inferSoundScript.sml in this directory.