go further with HOAS

remove the explicit logical variable environment, and use HOL variables
instead.
correction to Star

make it actually assert the assertions on the halves of the split state.
rewrite of mkdir axiom in new style