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.

.Note: I think `hp (hprop -> Empty) _` (or even `hp ~hprop _`) will suffice; the coercion to sortclass will pick up the `hproptype`, and typeclass inference should pick up `trunc_forall`.