---

Step * 1 1 of Lemma csm-ap-comp-term


1. Gamma : CubicalSet
2. Z : CubicalSet
3. A : {Gamma ⊢ _}
4. t : {Gamma ⊢ _:A}
5. I : Cname List
6. a : Z(I)
7. v : Z ⟶ Gamma
⊢ (t)v I a ∈ (fst((A)v)) I a
BY
{ (GenConclTerm ⌜(t)v⌝⋅ THENA Auto) }

1
1. Gamma : CubicalSet
2. Z : CubicalSet
3. A : {Gamma ⊢ _}
4. t : {Gamma ⊢ _:A}
5. I : Cname List
6. a : Z(I)
7. v : Z ⟶ Gamma
8. v1 : {Z ⊢ _:(A)v}
9. (t)v = v1 ∈ {Z ⊢ _:(A)v}
⊢ v1 I a ∈ (fst((A)v)) I a

---

Latex:

---

Latex:

1.  Gamma  :  CubicalSet
2.  Z  :  CubicalSet
3.  A  :  \{Gamma  \mvdash{}  \_\}
4.  t  :  \{Gamma  \mvdash{}  \_:A\}
5.  I  :  Cname  List
6.  a  :  Z(I)
7.  v  :  Z  {}\mrightarrow{}  Gamma
\mvdash{}  (t)v  I  a  \mmember{}  (fst((A)v))  I  a


By

---

Latex:
(GenConclTerm  \mkleeneopen{}(t)v\mkleeneclose{}\mcdot{}  THENA  Auto)

---

Home Index