---

Step * of Lemma empty-cubical-subset-term

∀[I:fset(ℕ)]. ∀[phi:Point(face_lattice(I))].
  ∀[X,A,B:Top].  (A = B ∈ {I,phi ⊢ _:X}) supposing phi = 0 ∈ Point(face_lattice(I))
BY
{ (Auto
   THEN EqTypeCD
   THEN (Auto THEN Try (RepeatFor 2 ((FunExt THENA Auto))))
   THEN Try (((InstLemma `empty-cubical-subset-I_cube` [⌜I⌝;⌜I@0⌝]⋅ THEN Auto) THEN D -1 THEN RWO "3<" 0 THEN Auto))) }

---

Latex:

---

Latex:
\mforall{}[I:fset(\mBbbN{})].  \mforall{}[phi:Point(face\_lattice(I))].    \mforall{}[X,A,B:Top].    (A  =  B)  supposing  phi  =  0


By

---

Latex:
(Auto
  THEN  EqTypeCD
  THEN  (Auto  THEN  Try  (RepeatFor  2  ((FunExt  THENA  Auto))))
  THEN  Try  (((InstLemma  `empty-cubical-subset-I\_cube`  [\mkleeneopen{}I\mkleeneclose{};\mkleeneopen{}I@0\mkleeneclose{}]\mcdot{}  THEN  Auto)
                        THEN  D  -1
                        THEN  RWO  "3<"  0
                        THEN  Auto)))

---

Home Index