progress updating holSemantics

work remaining: the two theorems out of a new type definition