---

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


1. Gamma : CubicalSet{j}
2. A : {Gamma ⊢ _}
3. phi : {Gamma ⊢ _:𝔽}
4. v : {Gamma, phi ⊢ _:A}
⊢ v = (v)iota ∈ {Gamma, phi ⊢ _:A}
BY
{ ((BLemma `cubical-term-equal` THENA Auto)
   THEN DVar `v'
   THEN RepeatFor 2 ((FunExt THENA Auto))
   THEN RepUR ``csm-ap-term csm-ap subset-iota`` 0
   THEN Auto) }

---

Latex:

---

Latex:

1.  Gamma  :  CubicalSet\{j\}
2.  A  :  \{Gamma  \mvdash{}  \_\}
3.  phi  :  \{Gamma  \mvdash{}  \_:\mBbbF{}\}
4.  v  :  \{Gamma,  phi  \mvdash{}  \_:A\}
\mvdash{}  v  =  (v)iota


By

---

Latex:
((BLemma  `cubical-term-equal`  THENA  Auto)
  THEN  DVar  `v'
  THEN  RepeatFor  2  ((FunExt  THENA  Auto))
  THEN  RepUR  ``csm-ap-term  csm-ap  subset-iota``  0
  THEN  Auto)

---

Home Index