[Iris-Club] Excluded middle leads to inconsistency

[Aleš Bizjak]

On 03 May 2017, at 10:47:51, Derek Dreyer wrote:

> You could replace the True at the beginning with emp.

Ah yes, then you just need emp ⊢ □True, which should be a valid property if we
want a sensible box.

-- Aleš