勒柯克:替代和依赖类型
问题描述:
我在一个奇怪的地方试图证明一个公式:勒柯克:替代和依赖类型
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
或结论改写。
我该如何继续?
答
subst x0
做了替换。