Step
*
1
of Lemma
ss-free-homotopic_weakening
.....wf.....
1. X : SeparationSpace
2. a : Point(X)
3. b : Point(X)
4. a ≡ b
⊢ λt.b ∈ Point(Path(X))
BY
{ ((RWO "path-ss-point" 0 THENA Auto) THEN MemTypeCD THEN Reduce 0 THEN Auto) }
Latex:
Latex:
.....wf.....
1. X : SeparationSpace
2. a : Point(X)
3. b : Point(X)
4. a \mequiv{} b
\mvdash{} \mlambda{}t.b \mmember{} Point(Path(X))
By
Latex:
((RWO "path-ss-point" 0 THENA Auto) THEN MemTypeCD THEN Reduce 0 THEN Auto)
Home
Index