勒柯克：替代和依赖类型

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做了替换。