---

Step * 2 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)
8. context-ok(X')
⊢ context-set(X') = context-set(X).type(allow(t)) ∈ CubicalSet'''
BY
{ (StrengthenEquation (-3)
   THEN (ApFunToHypEquands `Z' ⌜context-set(Z)⌝ ⌜CubicalSet'''⌝ (-1)⋅ THENA (D -1 THEN Auto))
   THEN NthHypEqTrans (-1)) }

1
.....assertion..... 
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)
8. context-ok(X')
9. X'
= update-context2(X;v;t)
∈ {z:?CubicalContext| (z = X' ∈ ?CubicalContext) ∧ (z = update-context2(X;v;t) ∈ ?CubicalContext)} 
10. context-set(X') = context-set(update-context2(X;v;t)) ∈ CubicalSet'''
⊢ context-set(update-context2(X;v;t)) = context-set(X).type(allow(t)) ∈ CubicalSet'''

---

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)
8.  context-ok(X')
\mvdash{}  context-set(X')  =  context-set(X).type(allow(t))


By

---

Latex:
(StrengthenEquation  (-3)
  THEN  (ApFunToHypEquands  `Z'  \mkleeneopen{}context-set(Z)\mkleeneclose{}  \mkleeneopen{}CubicalSet'''\mkleeneclose{}  (-1)\mcdot{}  THENA  (D  -1  THEN  Auto))
  THEN  NthHypEqTrans  (-1))

---

Home Index