---

Step * of Lemma context-adjoin-subset2

No Annotations
∀[H:j⊢]. ∀[phi:{H ⊢ _:𝔽}].  sub_cubical_set{j:l}(H, phi.𝕀; H.𝕀, (phi)p)
BY
{ Auto }

---

Latex:

---

Latex:
No  Annotations
\mforall{}[H:j\mvdash{}].  \mforall{}[phi:\{H  \mvdash{}  \_:\mBbbF{}\}].    sub\_cubical\_set\{j:l\}(H,  phi.\mBbbI{};  H.\mBbbI{},  (phi)p)


By

---

Latex:
Auto

---

Home Index