---

Step * 1 of Lemma context-set-update-context4


1. X : ?CubicalContext
2. context-ok(X)
3. [phi] : Provisional''''(cttTerm(context-set(X)))
4. X' : ?CubicalContext
5. X' = update-context4{i:l}(X;phi) ∈ ?CubicalContext
6. allowed(phi)
7. type(allow(phi))=𝔽
⊢ context-ok(X')
BY
{ ((RWO "-3" 0 THENA Auto)
   THEN RepUR ``context-ok update-context4 bind-provision`` 0
   THEN RepUR ``restrict-cubical-context allowed provision`` 0
   THEN Fold `allowed` 0
   THEN Fold `context-set` 0
   THEN (Unfold `cubical-context` 1 THEN UsquashCD)
   THEN Auto) }

---

Latex:

---

Latex:

1.  X  :  ?CubicalContext
2.  context-ok(X)
3.  [phi]  :  Provisional''''(cttTerm(context-set(X)))
4.  X'  :  ?CubicalContext
5.  X'  =  update-context4\{i:l\}(X;phi)
6.  allowed(phi)
7.  type(allow(phi))=\mBbbF{}
\mvdash{}  context-ok(X')


By

---

Latex:
((RWO  "-3"  0  THENA  Auto)
  THEN  RepUR  ``context-ok  update-context4  bind-provision``  0
  THEN  RepUR  ``restrict-cubical-context  allowed  provision``  0
  THEN  Fold  `allowed`  0
  THEN  Fold  `context-set`  0
  THEN  (Unfold  `cubical-context`  1  THEN  UsquashCD)
  THEN  Auto)

---

Home Index