---

Step * of Lemma update-context2_wf

No Annotations
∀[X:?CubicalContext]
  ∀[v:varname()]. ∀[t:Provisional''''(cttType(context-set(X)))].  (update-context2(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-context2` 0
   THEN MemCD
   THEN ((DSet (-1) THEN D -1) ORELSE Auto)
   THEN MemCD
   THEN Try (Declaration)
   THEN (DoSubsume THENL [Auto; (BLemma `provisional-subtype` THENW Auto)])) }

1
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))

---

Latex:

---

Latex:
No  Annotations
\mforall{}[X:?CubicalContext]
    \mforall{}[v:varname()].  \mforall{}[t:Provisional''''(cttType(context-set(X)))].
        (update-context2(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-context2`  0
  THEN  MemCD
  THEN  ((DSet  (-1)  THEN  D  -1)  ORELSE  Auto)
  THEN  MemCD
  THEN  Try  (Declaration)
  THEN  (DoSubsume  THENL  [Auto;  (BLemma  `provisional-subtype`  THENW  Auto)]))

---

Home Index