---

Step * of Lemma update-context2-ok

No Annotations
∀X:?CubicalContext
  (context-ok(X)
  ⇒ (∀[v:varname()]. ∀[t:Provisional''''(cttType(context-set(X)))].
        ∀X':?CubicalContext. ((X' = update-context2(X;v;t) ∈ ?CubicalContext) ⇒ {allowed(t) ⇒ context-ok(X')})))
BY
{ (InstLemma `context-set-update-context2` []
   THEN RepeatFor 3 ((ParallelLast' THENA Auto))
   THEN (InstLemma `provisional-type_wf` [⌜parm{i''''}⌝;⌜T:{context-set(X) ⊢''' _} × composition-structure{i''':l,
                                                                                                           i''':l}
                                                                                       (context-set(X); T)⌝]⋅
         THENA (Auto THEN DoSubsume THEN Auto)
         )
   THEN ParallelOp -2
   THEN RepeatFor 4 ((ParallelLast' THENA Auto))
   THEN Auto) }

---

Latex:

---

Latex:
No  Annotations
\mforall{}X:?CubicalContext
    (context-ok(X)
    {}\mRightarrow{}  (\mforall{}[v:varname()].  \mforall{}[t:Provisional''''(cttType(context-set(X)))].
                \mforall{}X':?CubicalContext.  ((X'  =  update-context2(X;v;t))  {}\mRightarrow{}  \{allowed(t)  {}\mRightarrow{}  context-ok(X')\})))


By

---

Latex:
(InstLemma  `context-set-update-context2`  []
  THEN  RepeatFor  3  ((ParallelLast'  THENA  Auto))
  THEN  (InstLemma  `provisional-type\_wf`  [\mkleeneopen{}parm\{i''''\}\mkleeneclose{};
              \mkleeneopen{}T:\{context-set(X)  \mvdash{}'''  \_\}  \mtimes{}  composition-structure\{i''':l,  i''':l\}(context-set(X);  T)\mkleeneclose{}]\mcdot{}
              THENA  (Auto  THEN  DoSubsume  THEN  Auto)
              )
  THEN  ParallelOp  -2
  THEN  RepeatFor  4  ((ParallelLast'  THENA  Auto))
  THEN  Auto)

---

Home Index