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


It's quite confusing to the reader stepping through the proof that `apply path_hprop` _appears_ to leave the goal unchanged, but omitting it breaks the proof.  In fact, of course, what it's done is insert invisible coercions, which the following `simpl` then reveals.  I wonder whether there is some way to fix this (this is not really directed at you, @marcbezem, any more than anyone else).