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


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


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
8.  v1  :  \{Z  \mvdash{}  \_:(A)v\}
9.  (t)v  =  v1
\mvdash{}  v1  I  a  \mmember{}  (fst((A)v))  I  a


By


Latex:
(D  -2  THEN  Auto)




Home Index