---

Step * 1 of Lemma csm-canonical-section-face-type-1

.....subterm..... T:t
5:n
1. I : fset(ℕ)
2. i : {i:ℕ| ¬i ∈ I} 
3. phi : 𝔽(I)
⊢ (i1)(s(phi)) = phi ∈ 𝔽(⋅)
BY
{ ((RWO "face-type-at" 0 THENA Auto)
   THEN RepUR ``face-presheaf`` -1
   THEN RepUR ``face-presheaf`` 0
   THEN RWW "fl-morph-comp2 s-comp-nc-1 fl-morph-id" 0⋅
   THEN Auto) }

---

Latex:

---

Latex:
.....subterm.....  T:t
5:n
1.  I  :  fset(\mBbbN{})
2.  i  :  \{i:\mBbbN{}|  \mneg{}i  \mmember{}  I\} 
3.  phi  :  \mBbbF{}(I)
\mvdash{}  (i1)(s(phi))  =  phi


By

---

Latex:
((RWO  "face-type-at"  0  THENA  Auto)
  THEN  RepUR  ``face-presheaf``  -1
  THEN  RepUR  ``face-presheaf``  0
  THEN  RWW  "fl-morph-comp2  s-comp-nc-1  fl-morph-id"  0\mcdot{}
  THEN  Auto)

---

Home Index