[Iris-Club] Frame-preserving update and double-negation

[Robbert Krebbers]

On 08/24/2016 07:30 PM, Ralf Jung wrote:
> That's cute.  We should put this somewhere in the repo.  Could you put
> it into some file (algebra/double_negation or so?)
If you want to keep track of such facts in the Iris repository, I would 
be in favor of putting them in an additional folder, together with 
things like program_logic/counter_examples.v.

Any suggestions for an appropriate name for this folder?