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 following worked:

Definition LEM := forall (A : Type) `{IsHProp A}, A + ~A.

Definition LEM_hProp_Bool (lem : LEM) (hprop : hProp) : Bool
  := match (lem hprop _) with inl _ => true | inr _ => false end.

NB1 ` before {IsHProp A} was necessary (what is this "`"? Is it "look it up in a larger scope"? 
NB2 the _ in (lem hprop _) was necessary, that's fine with me.
NB3 I'm more comfortable with the match as is than with if .. then .. else (if not Bool)