prove some inference rules correct
prove the 8 easy inference rules correct

(the hard ones are INST, INST_TYPE, and the context-update rules)