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

[Robbert Krebbers]

On 08/24/2016 09:04 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?
> base_logic/facts/ (following the new folder layout)?
Hmm, I would like the name of this folder to reflect that these 'facts' 
are not needed for the actual Iris logic, but are just there for 
informative purposes.