---

Step * of Lemma cubical-context_cumulativity

No Annotations
?CubicalContext ⊆r ?CubicalContext'
BY
{ (Unfold `cubical-context` 0
   THEN InstLemma `provisional-subtype` [⌜parm{i'''''}⌝;⌜CubicalContext⌝;⌜cubical_context{i':l}⌝]⋅
   THEN Auto) }

---

Latex:

---

Latex:
No  Annotations
?CubicalContext  \msubseteq{}r  ?CubicalContext'


By

---

Latex:
(Unfold  `cubical-context`  0
  THEN  InstLemma  `provisional-subtype`  [\mkleeneopen{}parm\{i'''''\}\mkleeneclose{};\mkleeneopen{}CubicalContext\mkleeneclose{};\mkleeneopen{}cubical\_context\{i':l\}\mkleeneclose{}]\mcdot{}
  THEN  Auto)

---

Home Index