---

Step * of Lemma context-subset-term-0

No Annotations
∀[Gamma:j⊢]. ∀[T:{Gamma ⊢ _}].  (Top ⊆r {Gamma, 0(𝔽) ⊢ _:T})
BY
{ (Intros THEN (D 0 THENA Auto)) }

1
.....subterm..... T:t
1:n
1. Gamma : CubicalSet{j}
2. T : {Gamma ⊢ _}
3. x : Top
⊢ x ∈ {Gamma, 0(𝔽) ⊢ _:T}

---

Latex:

---

Latex:
No  Annotations
\mforall{}[Gamma:j\mvdash{}].  \mforall{}[T:\{Gamma  \mvdash{}  \_\}].    (Top  \msubseteq{}r  \{Gamma,  0(\mBbbF{})  \mvdash{}  \_:T\})


By

---

Latex:
(Intros  THEN  (D  0  THENA  Auto))

---

Home Index