---

Step * 2 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))=𝔽
8. context-ok(X')
⊢ context-set(X') = context-set(X), term(allow(phi)) ∈ CubicalSet'''
BY
{ (StrengthenEquation (-4)
   THEN (Assert context-set(X') = context-set(update-context4{i:l}(X;phi)) ∈ CubicalSet''' BY
               (EquationFromHyp (-1) THEN Auto))
   THEN NthHypEqTrans (-1)
   THEN RepUR ``context-set update-context4 bind-provision restrict-cubical-context`` 0
   THEN (GenConcl ⌜term(allow(phi)) = a ∈ {context-set(X) ⊢ _:𝔽}⌝⋅ THENA Auto)
   THEN Thin (-1)
   THEN MoveToConcl (-1)) }

1
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))=𝔽
8. context-ok(X')
9. X'
= update-context4{i:l}(X;phi)
∈ {z:?CubicalContext| (z = X' ∈ ?CubicalContext) ∧ (z = update-context4{i:l}(X;phi) ∈ ?CubicalContext)} 
10. context-set(X') = context-set(update-context4{i:l}(X;phi)) ∈ CubicalSet'''
⊢ ∀a:{context-set(X) ⊢ _:𝔽}. ((fst(let X,vs,f = allow(X) in <X, a, vs, f>)) = fst(allow(X)), a ∈ CubicalSet''')

---

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


By

---

Latex:
(StrengthenEquation  (-4)
  THEN  (Assert  context-set(X')  =  context-set(update-context4\{i:l\}(X;phi))  BY
                          (EquationFromHyp  (-1)  THEN  Auto))
  THEN  NthHypEqTrans  (-1)
  THEN  RepUR  ``context-set  update-context4  bind-provision  restrict-cubical-context``  0
  THEN  (GenConcl  \mkleeneopen{}term(allow(phi))  =  a\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  Thin  (-1)
  THEN  MoveToConcl  (-1))

---

Home Index