---

Step * of Lemma update-context3_wf

No Annotations
∀[X:?CubicalContext]
  ∀[v:varname()]. ∀[t:Provisional''''(cttTerm(context-set(X)))].  (update-context3(X;v;t) ∈ ?CubicalContext) 
  supposing context-ok(X)
BY
{ (RepeatFor 2 (Intro)
   THEN (Assert context-set(X) ⊢''' BY
               Auto)
   THEN Intros
   THEN Unhide
   THEN All (Unfold `cubical-context`)
   THEN Unfold `update-context3` 0
   THEN MemCD
   THEN ((DSet (-1) THEN D -1) ORELSE Auto)
   THEN MemCD
   THEN Try (Declaration)
   THEN (DoSubsume THEN Try (Trivial))
   THEN (BLemma `provisional-subtype` THENW Auto)
   THEN (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:
No  Annotations
\mforall{}[X:?CubicalContext]
    \mforall{}[v:varname()].  \mforall{}[t:Provisional''''(cttTerm(context-set(X)))].
        (update-context3(X;v;t)  \mmember{}  ?CubicalContext) 
    supposing  context-ok(X)


By

---

Latex:
(RepeatFor  2  (Intro)
  THEN  (Assert  context-set(X)  \mvdash{}'''  BY
                          Auto)
  THEN  Intros
  THEN  Unhide
  THEN  All  (Unfold  `cubical-context`)
  THEN  Unfold  `update-context3`  0
  THEN  MemCD
  THEN  ((DSet  (-1)  THEN  D  -1)  ORELSE  Auto)
  THEN  MemCD
  THEN  Try  (Declaration)
  THEN  (DoSubsume  THEN  Try  (Trivial))
  THEN  (BLemma  `provisional-subtype`  THENW  Auto)
  THEN  (Assert  (fst(ctxt))  =  context-set(X)  BY
                          (Unfold  `context-set`  0  THEN  EquationFromHyp  8  THEN  Auto))
  THEN  RWO  "-1"  0
  THEN  Auto)

---

Home Index