---

Step * of Lemma subset-cubical-type-general

No Annotations
∀[X,Y:j⊢].  {X ⊢j _} ⊆r {Y ⊢j _} supposing sub_cubical_set{j:l}(Y; X)
BY
{ (Intros
   THEN (D 0 THENA Auto)
   THEN (InstLemma `subset-I_cube` [⌜X⌝;⌜Y⌝]⋅ THENA Auto)
   THEN (InstLemma `subset-restriction` [⌜X⌝;⌜Y⌝]⋅ THENA Auto)
   THEN RepeatFor 2 (PromoteHyp (-1) 3)
   THEN RepeatFor 2 (DVar `x')
   THEN (MemTypeCD THENW Auto)
   THEN All Reduce
   THEN Try ((MemCD THEN Auto))
   THEN RepeatFor 8 (ParallelLast)
   THEN RWO "4" (-1)
   THEN Auto) }

---

Latex:

---

Latex:
No  Annotations
\mforall{}[X,Y:j\mvdash{}].    \{X  \mvdash{}j  \_\}  \msubseteq{}r  \{Y  \mvdash{}j  \_\}  supposing  sub\_cubical\_set\{j:l\}(Y;  X)


By

---

Latex:
(Intros
  THEN  (D  0  THENA  Auto)
  THEN  (InstLemma  `subset-I\_cube`  [\mkleeneopen{}X\mkleeneclose{};\mkleeneopen{}Y\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (InstLemma  `subset-restriction`  [\mkleeneopen{}X\mkleeneclose{};\mkleeneopen{}Y\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  RepeatFor  2  (PromoteHyp  (-1)  3)
  THEN  RepeatFor  2  (DVar  `x')
  THEN  (MemTypeCD  THENW  Auto)
  THEN  All  Reduce
  THEN  Try  ((MemCD  THEN  Auto))
  THEN  RepeatFor  8  (ParallelLast)
  THEN  RWO  "4"  (-1)
  THEN  Auto)

---

Home Index