---

Step * of Lemma open_box_wf

∀[X:CubicalSet]. ∀[I,J:Cname List]. ∀[x:nameset(I)]. ∀[i:ℕ2].  (open_box(X;I;J;x;i) ∈ Type)
BY
{ ProveWfLemma }

---

Latex:

---

Latex:
\mforall{}[X:CubicalSet].  \mforall{}[I,J:Cname  List].  \mforall{}[x:nameset(I)].  \mforall{}[i:\mBbbN{}2].    (open\_box(X;I;J;x;i)  \mmember{}  Type)


By

---

Latex:
ProveWfLemma

---

Home Index