---

Step * of Lemma context-adjoin-subset

No Annotations
∀[X,Y:j⊢]. ∀[A:{Y ⊢ _}].  sub_cubical_set{[i | j]:l}(X.A; Y.A) supposing sub_cubical_set{j:l}(X; Y)
BY
{ Auto }

---

Latex:

---

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


By

---

Latex:
Auto

---

Home Index