This fact is deduced from reducibility. Unfortunately, this sometimes depends on the type of states being inhabited, so that this additional hypothesis sometimes appear.

Conflicts:
	docs/program-logic.tex

rename program_logic.{ownership -> wsat}. It really is about world satisfaction and invariants more than about ownership.

(forgot to add this to the previous commit...)

Initial proof by Jan-Oliver Kaiser, adapted by Robbert Krebbers.