We now have:

  Π★{map Q } ...
  Π★{set Q } ...

to differentiate between sets and maps.

* Clearly separate the file algebra/sts in three parts:
  1.) The definition of an STS, step relations, and closure stuff
  2.) The construction as a disjoint RA (this module should never be used)
  3.) The construction as a CMRA with many derived properties
* Turn stsT into a canonical structure so that we can make more of its arguments
  implicit.
* Rename the underlying step relation of STSs to prim_step (similar naming as
  for languages, but here in a module to avoid ambiguity)
* Refactor program_logic/sts by moving general properties of the STS CMRA to
  algebra/sts.v
* Make naming and use of modules in program_logic/sts more consistent with
  program_logic/auth and program_logic/saved_prop
* Prove setoid properties of all definitions in program_logic/sts

With nicely overloaded notations for sets and maps.

We only use wp_value in the end if the resulting goal is yet
another wp. Otherwise we may not be able to do a final view
shift (as observed by Ralf).

It now also reshapes expressions as values for contexts that need
values such as AppECtx.

Turns out it only holds as a view shift, not as an implication