unified treatment of PAxm/Oracle/Promise in basic proof term operations; refined promise/fulfill: maintain proper type instantiation, disallow term variables; thm_proof: uniform finish_proof before and after fulfill;