decidable equality for lifetimes
decidable equality for types
decidable equality for vectors
renamed transport to subst
judgment for consistency of a heap type with a context and map
moved Context for heap types into parameter position. saves typing
made some undeed parts of the shapes-preserve-types proof implicit
proved that well typed paths evaluate to well typed routs of the same type