Theorem reflect_b_P : forall b:bool,
   exists P:Prop, (b = true -> P) /\ (b = false -> ~P).
Proof.
  intros b.
  exists (b = true).
  destruct b; split; try firstorder; try congruence.
Qed.