sketch of more abstract embedding of first-order logic

Three things here:
  - Abstract out lifting a "propositional connective" with (D)Lift operators.
  - Use printing/parsing overloads to reuse nice syntax for the
    propositional connectives.
  - Use something like Higher-order Abstract Syntax for the quantifiers.

I'm pretty unsure that I've got the semantics right, especially for the
quantifiers. I haven't tried to rework the axioms yet.
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
change Var to Val and make it take a value set

rather than a single value, since expressions denote sets of values and
sometimes we want that full expressivity with logical vars.

also, tweak the Entry assertion.
rewrite the mkdir_root axiom in the new style
tweak the notes about how to interpret the variables
rewrite rename_dir_move_not_exist in the new style
bit more syntax tweaking and another axiom translation
bit more syntax, another axiom
another abbreviation, another axiom
more syntax and another axiom
few more axioms, and nicer syntax for file links
finish rewriting the axioms
tweaks

mostly just names of things.
but also, ensure eval_exp only returns sets of values of the same type.
Added some directory assertion checks.
Some directory heap assertion checks.
remove program variable references

therefore expression evaluation doesn't depend on the program
environment any more, and neither do directory assertions.

also remove ExpCell.
add extra condition to DContextApplication
work through some of the sanity tests