Fixed False_hp, added Negation_hp

Question: where to place (in HProp.v, Bool.v, Misc.v, HoTTBookExercises.v, or elsewhere)?
Require Import Bool.
(** canonical map from Bool to hProp *)
Definition Bool_to_hProp (b : Bool) : hProp
  := if b then Unit_hp else False_hp.

In HProp.v this gave an unexpected error ("Bool not found in the current environment") with the latest coq-scripts @ a87e3ca, while it had been typechecked correctly before.

Nit: It's slightly preferred, I think to not add these extra lines at the end and simply have one trailing newline.  But this will not block merging.