---

Step * of Lemma constrained-cubical-term-0

No Annotations
∀[Gamma:j⊢]. ∀[A:{Gamma ⊢ _}]. ∀[t:Top]. ∀[x:{Gamma ⊢ _:A}].  (x ∈ {Gamma ⊢ _:A[0(𝔽) |⟶ t]})
BY
{ (Intros THEN MemTypeCD THEN Try (Trivial)) }

1
.....set predicate..... 
1. Gamma : CubicalSet{j}
2. A : {Gamma ⊢ _}
3. t : Top
4. x : {Gamma ⊢ _:A}
⊢ t = x ∈ {Gamma, 0(𝔽) ⊢ _:A}

2
.....wf..... 
1. Gamma : CubicalSet{j}
2. A : {Gamma ⊢ _}
3. t : Top
4. x : {Gamma ⊢ _:A}
5. a : {Gamma ⊢ _:A}
⊢ istype(t = a ∈ {Gamma, 0(𝔽) ⊢ _:A})

---

Latex:

---

Latex:
No  Annotations
\mforall{}[Gamma:j\mvdash{}].  \mforall{}[A:\{Gamma  \mvdash{}  \_\}].  \mforall{}[t:Top].  \mforall{}[x:\{Gamma  \mvdash{}  \_:A\}].    (x  \mmember{}  \{Gamma  \mvdash{}  \_:A[0(\mBbbF{})  |{}\mrightarrow{}  t]\})


By

---

Latex:
(Intros  THEN  MemTypeCD  THEN  Try  (Trivial))

---

Home Index