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


@mikeshulman My experience: total confusion during at least one hour. About etc. gives type
... X = Y -> X = Y for pathhprop, which made me think of a bug. I further tried:

Lemma foo `{Funext} : Unit_hp = Unit_hp.
Proof. apply path_hprop. exact (idpath Unit_hp).

which complains about the universe levels. Finally, I tried simpl, which worked.

@jasongross For using Local Open Scope long_type_scope I should better understand what I'm doing then (but that's never a disadvantage).