Minimized problem with `rewrite decide_True` and ssreflect

decide_True_broke.v

(*
Tested with:
Coq 8.15.0, Iris dev.2022-01-24.0.72a4bd62.
Coq 8.16.0, Iris 4.0.0
*)

From iris.prelude Require Import prelude.

Lemma bar : (if decide (0 = 0) then 0 else 0) = 0.
Proof.
  Succeed by rewrite ->decide_True.
  Fail rewrite decide_True.
  Fail rewrite (decide_True (A := nat) _ 0).
  Fail rewrite (@decide_True nat (@eq nat 0 0) _ _ _ _).
  set (dec := decide_rel _ _ _).
  Fail rewrite decide_True.
  Fail rewrite (decide_True (A := nat) _ 0).
  Fail rewrite (@decide_True nat (@eq nat 0 0) _ _ _ _).
  Succeed rewrite (@decide_True nat (@eq nat 0 0) dec _ _ _).
Abort.

(* 
  I already tried to shadow the lemma the way ssreflect prefers it:
Set Implicit Arguments.
Lemma decide_True (A : Type) (P : Prop) (H : Decision P) (x y : A) :
  P → (if decide P then x else y) = x.
Proof.
  intros. by apply decide_True.
Qed. *)