Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2006-03-10 11:32:08 -0800 (Fri, 10 Mar 2006)
Revision: 8867
Log message:

      Define a predicate proof_check{'r; 'assums; 'goal; 'witness} that
      says that a proof step checks against rule 'r.