---

Step * 1 of Lemma update-context2_wf


1. X : Provisional''''(CubicalContext)
2. context-ok(X)
3. context-set(X) ⊢'''
4. v : varname()
5. t : Provisional''''(cttType(context-set(X)))
6. ctxt : CubicalContext
7. allowed(X)
8. ctxt = allow(X) ∈ CubicalContext
9. t = t ∈ Provisional''''(cttType(context-set(X)))
⊢ cttType(context-set(X)) ⊆r ctt-type-meaning1{i:l}(fst(ctxt))
BY
{ ((Assert (fst(ctxt)) = context-set(X) ∈ CubicalSet''' BY
          (Unfold `context-set` 0 THEN EquationFromHyp 8 THEN Auto))
   THEN RWO "-1" 0
   THEN Auto) }

---

Latex:

---

Latex:

1.  X  :  Provisional''''(CubicalContext)
2.  context-ok(X)
3.  context-set(X)  \mvdash{}'''
4.  v  :  varname()
5.  t  :  Provisional''''(cttType(context-set(X)))
6.  ctxt  :  CubicalContext
7.  allowed(X)
8.  ctxt  =  allow(X)
9.  t  =  t
\mvdash{}  cttType(context-set(X))  \msubseteq{}r  ctt-type-meaning1\{i:l\}(fst(ctxt))


By

---

Latex:
((Assert  (fst(ctxt))  =  context-set(X)  BY
                (Unfold  `context-set`  0  THEN  EquationFromHyp  8  THEN  Auto))
  THEN  RWO  "-1"  0
  THEN  Auto)

---

Home Index