---

Step * of Lemma context-1-subset

No Annotations
∀[Gamma:j⊢]. sub_cubical_set{j:l}(Gamma; Gamma, 1(𝔽))
BY
{ (Auto THEN UnfoldTopAb 0) }

1
1. Gamma : CubicalSet{j}
⊢ 1(Gamma) ∈ Gamma j⟶ Gamma, 1(𝔽)

---

Latex:

---

Latex:
No  Annotations
\mforall{}[Gamma:j\mvdash{}].  sub\_cubical\_set\{j:l\}(Gamma;  Gamma,  1(\mBbbF{}))


By

---

Latex:
(Auto  THEN  UnfoldTopAb  0)

---

Home Index