---

Step * of Lemma lift-id-faces_wf

∀[X:CubicalSet]. ∀[A:{X ⊢ _}]. ∀[a,b:{X ⊢ _:A}]. ∀[I:Cname List]. ∀[J:nameset(I) List]. ∀[x:nameset(I)]. ∀[i:ℕ2].
∀[alpha:X(I)]. ∀[box:A-open-box(X;(Id_A a b);I;alpha;J;x;i)].
  (lift-id-faces(X;A;I;alpha;box) ∈ A-open-box(X;A;[fresh-cname(I) / I];iota(fresh-cname(I))(alpha);J;x;i))
BY
{ (InstLemma `lift-id-faces-wf` []
   THEN RepeatFor 10 (ParallelLast')
   THEN RepUR ``add-fresh-cname iota\'`` -1
   THEN CallByValueReduce (-1)
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[X:CubicalSet].  \mforall{}[A:\{X  \mvdash{}  \_\}].  \mforall{}[a,b:\{X  \mvdash{}  \_:A\}].  \mforall{}[I:Cname  List].  \mforall{}[J:nameset(I)  List].
\mforall{}[x:nameset(I)].  \mforall{}[i:\mBbbN{}2].  \mforall{}[alpha:X(I)].  \mforall{}[box:A-open-box(X;(Id\_A  a  b);I;alpha;J;x;i)].
    (lift-id-faces(X;A;I;alpha;box)  \mmember{}  A-open-box(X;A;[fresh-cname(I)  / 
                                                                                                        I];iota(fresh-cname(I))(alpha);J;x;i))


By

---

Latex:
(InstLemma  `lift-id-faces-wf`  []
  THEN  RepeatFor  10  (ParallelLast')
  THEN  RepUR  ``add-fresh-cname  iota\mbackslash{}'``  -1
  THEN  CallByValueReduce  (-1)
  THEN  Auto)

---

Home Index