---

Step * of Lemma A-face-compatible_wf

∀[X:CubicalSet]. ∀[A:{X ⊢ _}]. ∀[I:Cname List]. ∀[alpha:X(I)]. ∀[f1,f2:A-face(X;A;I;alpha)].
  (A-face-compatible(X;A;I;alpha;f1;f2) ∈ ℙ)
BY
{ (Intros
   THEN Unhide
   THEN Unfold `A-face-compatible` 0
   THEN RepeatFor 2 (D -2)
   THEN RepeatFor 2 (D -1)
   THEN Reduce 0
   THEN ((Assert (x:=i) ∈ name-morph(I-[x1];I-[x; x1]) BY
                (SubsumeC ⌜name-morph(I-[x1];I-[x1]-[x])⌝⋅ THEN Auto THEN RWO "list-diff2-sym" 0 THEN Auto))
         THEN (Assert (x1:=i1) ∈ name-morph(I-[x];I-[x; x1]) BY
                     (SubsumeC ⌜name-morph(I-[x];I-[x]-[x1])⌝⋅ THEN Auto THEN RWO "list-diff2" 0 THEN Auto))
         )
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[X:CubicalSet].  \mforall{}[A:\{X  \mvdash{}  \_\}].  \mforall{}[I:Cname  List].  \mforall{}[alpha:X(I)].  \mforall{}[f1,f2:A-face(X;A;I;alpha)].
    (A-face-compatible(X;A;I;alpha;f1;f2)  \mmember{}  \mBbbP{})


By

---

Latex:
(Intros
  THEN  Unhide
  THEN  Unfold  `A-face-compatible`  0
  THEN  RepeatFor  2  (D  -2)
  THEN  RepeatFor  2  (D  -1)
  THEN  Reduce  0
  THEN  ((Assert  (x:=i)  \mmember{}  name-morph(I-[x1];I-[x;  x1])  BY
                            (SubsumeC  \mkleeneopen{}name-morph(I-[x1];I-[x1]-[x])\mkleeneclose{}\mcdot{}
                              THEN  Auto
                              THEN  RWO  "list-diff2-sym"  0
                              THEN  Auto))
              THEN  (Assert  (x1:=i1)  \mmember{}  name-morph(I-[x];I-[x;  x1])  BY
                                      (SubsumeC  \mkleeneopen{}name-morph(I-[x];I-[x]-[x1])\mkleeneclose{}\mcdot{}
                                        THEN  Auto
                                        THEN  RWO  "list-diff2"  0
                                        THEN  Auto))
              )
  THEN  Auto)

---

Home Index