get replTheory to build

just change a type annotation
make explicit op <> Opapp in one of the app cases

this is implicitly true because of do_app's definition, but this way the
determinism proof doesn't need to expand that definition.
fix up evalPropsTheory