Solution to Exc. 3.9

The first two lemmas could move to HProp.v.
When a standard reference to LEM becomes available, I will adapt to that.