---

Step * of Lemma context-subset-term-1

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

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

---

Latex:

---

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


By

---

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

---

Home Index