---

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


1. X : ?CubicalContext
2. context-ok(X)
3. [v] : varname()
4. [t] : Provisional''''(cttType(context-set(X)))
5. X' : ?CubicalContext
6. X' = update-context2(X;v;t) ∈ ?CubicalContext
7. allowed(t)
⊢ context-ok(X')
BY
{ ((RWO "-2" 0 THENA Auto)
   THEN RepUR ``update-context2 bind-provision provision context-ok`` 0
   THEN RepUR ``update-cubical-context2`` 0
   THEN Unfold `cubical-context` 1
   THEN UsquashCD
   THEN Auto) }

---

Latex:

---

Latex:

1.  X  :  ?CubicalContext
2.  context-ok(X)
3.  [v]  :  varname()
4.  [t]  :  Provisional''''(cttType(context-set(X)))
5.  X'  :  ?CubicalContext
6.  X'  =  update-context2(X;v;t)
7.  allowed(t)
\mvdash{}  context-ok(X')


By

---

Latex:
((RWO  "-2"  0  THENA  Auto)
  THEN  RepUR  ``update-context2  bind-provision  provision  context-ok``  0
  THEN  RepUR  ``update-cubical-context2``  0
  THEN  Unfold  `cubical-context`  1
  THEN  UsquashCD
  THEN  Auto)

---

Home Index