Coq中如何从existT等式推导原项相等？

我在依赖类型的Inductive定义上执行inversion H策略后，得到了形如existT ... n = existT ... n'的假设，想从中推导出n = n'（非依赖类型下这个过程会自动完成）。

具体来说，我认为以下引理应当成立，但Coq并未自动推导：

Lemma example3 (n n' : nat) :
  @existT Set (fun x => x) nat n = @existT Set (fun x => x) nat n' -> n = n'.
Proof.
  (* is that possible? *)

我觉得这应该是成立的，但该如何证明？如果不成立，原因是什么？

使用的Coq版本信息：

$ coqc --version                                                                                                                                                            mathieu-laptop
The Rocq Prover, version 9.0.0
compiled with OCaml 4.14.1

这个引理是成立的，可以通过以下几种方式证明：

方法1：使用injection策略提取等式 #

existT是依赖对（sigma类型）的构造子，对于这类依赖类型的等式，injection策略可以直接提取出底层参数的等式：

Lemma example3 (n n' : nat) :
  @existT Set (fun x => x) nat n = @existT Set (fun x => x) nat n' -> n = n'.
Proof.
  intro H.
  injection H.
  auto.
Qed.

方法2：使用destruct策略拆解依赖等式 #

直接对等式假设执行destruct，依赖类型的等式会自动将参数n和n'统一，后续直接用自反性证明即可：

Lemma example3 (n n' : nat) :
  @existT Set (fun x => x) nat n = @existT Set (fun x => x) nat n' -> n = n'.
Proof.
  intro H.
  destruct H.
  reflexivity.
Qed.

为什么Coq没有自动推导？ #

非依赖类型的等式（比如普通的pair nat nat）中，Coq可以自动识别构造子参数的等价性，但依赖类型的等式涉及类型层面的约束，Coq不会自动完成这类底层参数的等式提取，需要显式使用injection、destruct等策略拆解依赖等式，才能得到目标的参数相等关系。

内容的提问来源于stack exchange，提问作者Mathieu Paturel