Surprising definitional equality between empty matches from irrelevant to relevant at different indices

[SkySkimmer]

Inductive T : bool -> SProp := .

Goal forall (x:T true) (y:T false), match x return bool with end = match y return bool with end.
Proof.
  intros.
  reflexivity.
Qed.

I don't know if there's a way to break consistency or subject reduction or some other deisrable property from this, but it's not implied by the proof irrelevance rule "if x and y are at the same SProp type then they're convertible" so it's a bug.

[SkySkimmer]

NB: a presentation using eliminators instead of matches would not encounter this issue as the terms to compare are T_rec _ true x and T_rec _ false x, ie the indices are present.