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


My suggestions/ideas are:
For people reading the proof:
Have `Open Scope long_type_scope` and a comment about it.  This should make `apply path_hprop` change the goal.

For people developing proofs:
Improve Coq's error messages so that the error that you get when you leave out the `apply path_hprop` is sufficiently informative and not confusing.