Inductive type bool from Coq's Init.Datatypes

[benediktahrens]

We are using the booleans of Coq.Init.Datatypes, which are defined as an inductive type:

Inductive bool : Set :=
  | true : bool
  | false : bool.

Should we try replacing it by unit \coprod unit? Is the alternative definition of bool as coproduct already given somewhere?