Some lemmas and instances broke because of
  1. well-foundness of dexpr and dcexpr is parameterized by the set of variable names.
  2. the well-foundness of dloc takes now into account offsets