fix proof of t9
pull out empty_heap as a separate definition
change DirCell semantics to require a ProgValue Path

rather than a PathValue