work on holSemantics

done the term/type cases; the inference rule cases are next.