---

Step * 1 of Lemma context-subset-term-1

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

1
1. Gamma : CubicalSet{j}
2. T : {Gamma ⊢ _}
3. x : I:fset(ℕ) ⟶ a:Gamma(I) ⟶ T(a)
4. ∀I,J:fset(ℕ). ∀f:J ⟶ I. ∀a:Gamma(I).  ((x I a a f) = (x J f(a)) ∈ T(f(a)))
⊢ x ∈ {Gamma, 1(𝔽) ⊢ _:T}

---

Latex:

---

Latex:
.....subterm.....  T:t
1:n
1.  Gamma  :  CubicalSet\{j\}
2.  T  :  \{Gamma  \mvdash{}  \_\}
3.  x  :  \{Gamma  \mvdash{}  \_:T\}
\mvdash{}  x  \mmember{}  \{Gamma,  1(\mBbbF{})  \mvdash{}  \_:T\}


By

---

Latex:
DVar  `x'

---

Home Index