Coq: substitution and dependent types

Question

I am at an odd place trying to prove an equation:

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

What I want to do is to use H to substitute x for x0 everywhere. The rest of the proof would be easy, because I have:

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

However, rewrite H in * fails, and I cannot rewrite in either s1 or the conclusion separately.

How should I proceed ?

Answer 1

subst x0 did the substitution.