---

Step * of Lemma update-context4_wf

No Annotations
∀[X:?CubicalContext]
  ∀[phi:Provisional''''(cttTerm(context-set(X)))]. (update-context4{i:l}(X;phi) ∈ ?CubicalContext) 
  supposing context-ok(X)
BY
{ (Intros
   THEN Unhide
   THEN RepUR ``update-context4 cubical-context`` 0
   THEN (Assert istype({t:CubicalContext| allowed(X) ∧ (t = allow(X) ∈ CubicalContext)} ) BY
               (Fold `context-ok` 0 THEN Auto))
   THEN (MemCD THENA Auto)) }

1
.....subterm..... T:t
1:n
1. X : ?CubicalContext
2. context-ok(X)
3. phi : Provisional''''(cttTerm(context-set(X)))
4. istype({t:CubicalContext| allowed(X) ∧ (t = allow(X) ∈ CubicalContext)} )
⊢ X ∈ provisional-type{i 4:l}(CubicalContext)

2
.....subterm..... T:t
2:n
1. X : ?CubicalContext
2. context-ok(X)
3. phi : Provisional''''(cttTerm(context-set(X)))
4. istype({t:CubicalContext| allowed(X) ∧ (t = allow(X) ∈ CubicalContext)} )
5. ctxt : {t:CubicalContext| allowed(X) ∧ (t = allow(X) ∈ CubicalContext)} 
⊢ restrict-cubical-context{i:l}(ctxt;phi) ∈ provisional-type{i 4:l}(CubicalContext)

---

Latex:

---

Latex:
No  Annotations
\mforall{}[X:?CubicalContext]
    \mforall{}[phi:Provisional''''(cttTerm(context-set(X)))].  (update-context4\{i:l\}(X;phi)  \mmember{}  ?CubicalContext) 
    supposing  context-ok(X)


By

---

Latex:
(Intros
  THEN  Unhide
  THEN  RepUR  ``update-context4  cubical-context``  0
  THEN  (Assert  istype(\{t:CubicalContext|  allowed(X)  \mwedge{}  (t  =  allow(X))\}  )  BY
                          (Fold  `context-ok`  0  THEN  Auto))
  THEN  (MemCD  THENA  Auto))

---

Home Index