Lemmas 3.3.2 and 3.3.3 and Exc. 3.9

Lemmas 3.3.2 and 3.3.3 added to HProp
Backrefs added to HoTTBook
Solution to Exc.3.9 added to HoTTBookExercises


The fact that you end up with two witnesses of `hprop` is a clue that there's some redundancy here.  If you `unfold LEM_hProp_Bool` before the first `elim (lem hprop _)` (on line 434), then you won't need the second `elim (lem hprop _)` and you won't end up with the redundant `useless` (and you can eliminate some unneeded subgoals later on too).