DEDUCT_ANTISYM case of proves_IMP

and looking at the remainder, will probably need
  - connections between the INSTs and VSUBSTs in either world
  - something that says term_ok is preserved under consing a (good) definition
  - something that says everything in a context_ok context is term_ok