---

Step * of Lemma face-compatible-symmetry

∀[X:CubicalSet]. ∀[I:Cname List]. ∀[f1,f2:I-face(X;I)].  (face-compatible(X;I;f1;f2) ⇒ face-compatible(X;I;f2;f1))
BY
{ (Auto
   THEN UseWitness ⌜λx.Ax⌝⋅
   THEN RepeatFor 2 (D -3)
   THEN RepeatFor 2 (D -2)
   THEN All (RepUR  ``face-compatible``)
   THEN Auto
   THEN D -2
   THEN Auto) }

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])
9. x2 : ¬(x1 = x ∈ Cname)
10. (x1:=f7)(f5) = (x:=f4)(f8) ∈ X(I-[x; x1])
⊢ (x:=f4)(f8) = (x1:=f7)(f5) ∈ X(I-[x1; x])

---

Latex:

---

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


By

---

Latex:
(Auto
  THEN  UseWitness  \mkleeneopen{}\mlambda{}x.Ax\mkleeneclose{}\mcdot{}
  THEN  RepeatFor  2  (D  -3)
  THEN  RepeatFor  2  (D  -2)
  THEN  All  (RepUR    ``face-compatible``)
  THEN  Auto
  THEN  D  -2
  THEN  Auto)

---

Home Index