finish updating holSemantics
package up soundness theorem for stateful inference system