---

Step * 2 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))=𝔽
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''')
BY
{ (Unfold `context-set` 0 THEN (GenConclTerm ⌜allow(X)⌝⋅ THENA Auto) THEN RepeatFor 2 (D -2) THEN Reduce 0 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{}
8.  context-ok(X')
9.  X'  =  update-context4\{i:l\}(X;phi)
10.  context-set(X')  =  context-set(update-context4\{i:l\}(X;phi))
\mvdash{}  \mforall{}a:\{context-set(X)  \mvdash{}  \_:\mBbbF{}\}.  ((fst(let  X,vs,f  =  allow(X)  in  <X,  a,  vs,  f>))  =  fst(allow(X)),  a)


By

---

Latex:
(Unfold  `context-set`  0
  THEN  (GenConclTerm  \mkleeneopen{}allow(X)\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  RepeatFor  2  (D  -2)
  THEN  Reduce  0
  THEN  Auto)

---

Home Index