如何在Coq中处理依赖类型相等证明（Sigma类型）？卡壳引理求解

我一直在尝试证明这个引理（是我所需内容的抽象版本），但似乎陷入了依赖类型错误。我给出了初步的证明尝试（如下所示），但在处理sval表达式的相等性时不知如何推进，恳请提供建议？

From Coq Require Import Init.Prelude Unicode.Utf8.
From mathcomp Require Import all_ssreflect.

Require Import Coq.Logic.Classical.

Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.

Lemma oStar_perm_choiceTT : 
  forall (T : finType) (u : {set T}) (o : T) (o2 : {o | o \in u}) (ot : o \in u),
  o = sval ((if o \in u as x return ((o \in u) = x → {o : T | o \in u})
             then [eta exist (λ o : T, o \in u) o]
             else fun=> o2)
              (erefl (o \in u))).
Proof.
move=> T u o.
case=> o2 p ou.
have foo : o = sval (exist (fun o => o \in u) o ou) by [].
rewrite [LHS]foo.
apply/eq_sig_hprop_iff => /=; first by move=> x; apply: Classical_Prop.proof_irrelevance.

内容的提问来源于stack exchange，提问作者Pierre Jouvelot