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


I think it's preferred to pass the type rather than the proof of it being an hprop; write `lem (hproptype hprop) _` or just `lem hprop _` (using the fact that `hproptype` is a coercion).  If you define `LEM` as `forall (A : Type) `{IsHProp A}, A + ~A`, you might even be able to just write `lem hprop` (and have the `_` be inserted automatically).

Additionally, you can write the `match` as `if lem hprop _ then true else false`.