---

Step * 2 1 of Lemma context-set-update-context3

.....assertion..... 
1. X : ?CubicalContext
2. context-ok(X)
3. v : varname()
4. t : Provisional''''(cttTerm(context-set(X)))
5. X' : ?CubicalContext
6. X' = update-context3(X;v;t) ∈ ?CubicalContext
7. allowed(t)
8. context-ok(X')
9. X'
= update-context3(X;v;t)
∈ {z:?CubicalContext| (z = X' ∈ ?CubicalContext) ∧ (z = update-context3(X;v;t) ∈ ?CubicalContext)} 
10. context-set(X') = context-set(update-context3(X;v;t)) ∈ CubicalSet'''
⊢ context-set(update-context3(X;v;t)) = context-set(X).type(allow(t)) ∈ CubicalSet'''
BY
{ (RepUR ``update-context3 bind-provision update-cubical-context2 context-set`` 0
   THEN ((GenConclTerm ⌜allow(t)⌝⋅ THENA Auto) THEN Thin  (-1))
   THEN MoveToConcl (-1)
   THEN Unfold `context-set` 0
   THEN (GenConclTerm ⌜allow(X)⌝⋅ THENA Auto)
   THEN Thin  (-1)
   THEN (D -1 THEN Reduce 0)
   THEN (D 0 THENA Auto)) }

1
1. X : ?CubicalContext
2. context-ok(X)
3. v : varname()
4. t : Provisional''''(cttTerm(context-set(X)))
5. X' : ?CubicalContext
6. X' = update-context3(X;v;t) ∈ ?CubicalContext
7. allowed(t)
8. context-ok(X')
9. X'
= update-context3(X;v;t)
∈ {z:?CubicalContext| (z = X' ∈ ?CubicalContext) ∧ (z = update-context3(X;v;t) ∈ ?CubicalContext)} 
10. context-set(X') = context-set(update-context3(X;v;t)) ∈ CubicalSet'''
11. X1 : CubicalSet'''
12. v2 : vs:varname() List × ({v:varname()| (v ∈ vs)}  ⟶ cttTerm(X1))
13. v1@0 : cttTerm(X1)
⊢ (fst(let lvl,A,_ = v1@0 in update-context-lvl(<X1, v2>;lvl;A;v))) = X1.type(v1@0) ∈ CubicalSet'''

---

Latex:

---

Latex:
.....assertion..... 
1.  X  :  ?CubicalContext
2.  context-ok(X)
3.  v  :  varname()
4.  t  :  Provisional''''(cttTerm(context-set(X)))
5.  X'  :  ?CubicalContext
6.  X'  =  update-context3(X;v;t)
7.  allowed(t)
8.  context-ok(X')
9.  X'  =  update-context3(X;v;t)
10.  context-set(X')  =  context-set(update-context3(X;v;t))
\mvdash{}  context-set(update-context3(X;v;t))  =  context-set(X).type(allow(t))


By

---

Latex:
(RepUR  ``update-context3  bind-provision  update-cubical-context2  context-set``  0
  THEN  ((GenConclTerm  \mkleeneopen{}allow(t)\mkleeneclose{}\mcdot{}  THENA  Auto)  THEN  Thin    (-1))
  THEN  MoveToConcl  (-1)
  THEN  Unfold  `context-set`  0
  THEN  (GenConclTerm  \mkleeneopen{}allow(X)\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  Thin    (-1)
  THEN  (D  -1  THEN  Reduce  0)
  THEN  (D  0  THENA  Auto))

---

Home Index