---

Step * 1 2 of Lemma csm-ap-interval-1-adjoin-lemma

.....subterm..... T:t
2:n
1. H : CubicalSet{j}
2. I : fset(ℕ)
3. v : H(I)
4. j : {i:ℕ| ¬i ∈ I} 
⊢ (<j> s(v) (j1)) = (1(𝕀) I v) ∈ 𝕀((j1)(s(v)))
BY
{ ((RWO "interval-type-at-is-point" 0 THENA Auto)
   THEN RepUR ``interval-1`` 0
   THEN (RWO "interval-type-ap-inc" 0 THENA Auto)
   THEN RWO  "nc-1-lemma2" 0
   THEN Auto) }

---

Latex:

---

Latex:
.....subterm.....  T:t
2:n
1.  H  :  CubicalSet\{j\}
2.  I  :  fset(\mBbbN{})
3.  v  :  H(I)
4.  j  :  \{i:\mBbbN{}|  \mneg{}i  \mmember{}  I\} 
\mvdash{}  (<j>  s(v)  (j1))  =  (1(\mBbbI{})  I  v)


By

---

Latex:
((RWO  "interval-type-at-is-point"  0  THENA  Auto)
  THEN  RepUR  ``interval-1``  0
  THEN  (RWO  "interval-type-ap-inc"  0  THENA  Auto)
  THEN  RWO    "nc-1-lemma2"  0
  THEN  Auto)

---

Home Index