`rewrite decide_True` does not work with ssreflect rewritintg

Code says it all:

Lemma bar : (if decide (0 = 0) then 0 else 0) = 0.
Proof.
  Succeed by rewrite ->decide_True.
  Fail rewrite decide_True.
  [...]

Because of issues like this, @msammler @Blaisorblade and me now have a general suspicion against decide and prefer bool_decide wherever possible.

With bool_decide P one cannot do destruct and get a proof of P/¬P, but the case_bool_decide tactic handles that situation nicely. I never ran into situations where I wished I would have used decide instead of bool_decide. Hypothetically, if there are 2 bool_decide in the goal, case_bool_decide does not provide enough control to figure out which one to destruct, but one could imagine a case_bool_deice pat that pattern-matches P against pat to solve this problem.

So that leaves the question:

• Can we fix rewrite decide_True?
• Should we replace decide by bool_decide entirely / wherever possible, to steer people towards the more reliable option? It is very rare that you actually need the proof term, so arguably the version that returns bool should be the default.