Coq：替换和依赖类型

Question

我在一个奇怪的地方试图证明一个等式：

1 subgoals
A : Type
s : set A
x : A
s0 : s x
x0 : A
s1 : s x0
H : x0 = x
______________________________________(1/1)
stv s x0 s1 = stv s x s0

我想做的是用H到处用x代替x0。其余的证明会很简单，因为我有：

Definition set (A : Type) := A -> Prop.
Axiom proof_irrelevance: forall (P:Prop) (p1:P) (p2:P), p1 = p2.

然而，rewrite H in *失败了，我无法在s1或结论中单独重写。

我应该如何进行？

Answer 1

subst x0 进行了替换。