---

Step * of Lemma context-adjoin-subset1

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

---

Latex:

---

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


By

---

Latex:
Auto

---

Home Index