---

Step * of Lemma sq_stable__face-compatible

∀X:CubicalSet. ∀I:Cname List. ∀f1,f2:I-face(X;I).  SqStable(face-compatible(X;I;f1;f2))
BY
{ (xxxAutoxxx THEN RepeatFor 2 (D -2) THEN RepeatFor 2 (D -1) THEN RepUR ``face-compatible`` 0) }

1
1. X : CubicalSet
2. I : Cname List
3. x : nameset(I)
4. f4 : ℕ2
5. f5 : X(I-[x])
6. x1 : nameset(I)
7. f7 : ℕ2
8. f8 : X(I-[x1])
⊢ SqStable((¬(x = x1 ∈ Cname)) ⇒ ((x1:=f7)(f5) = (x:=f4)(f8) ∈ X(I-[x; x1])))

---

Latex:

---

Latex:
\mforall{}X:CubicalSet.  \mforall{}I:Cname  List.  \mforall{}f1,f2:I-face(X;I).    SqStable(face-compatible(X;I;f1;f2))


By

---

Latex:
(xxxAutoxxx  THEN  RepeatFor  2  (D  -2)  THEN  RepeatFor  2  (D  -1)  THEN  RepUR  ``face-compatible``  0)

---

Home Index