---

Step * of Lemma trivial-section_wf

∀[I:fset(ℕ)]. ∀[X:Top]. ∀[phi:Point(face_lattice(I))].  () ∈ {I,phi ⊢ _:X} supposing phi = 0 ∈ Point(face_lattice(I))
BY
{ (Auto
   THEN MemTypeCD
        THEN (Auto
              THEN Try (RepeatFor 2 ((FunExt THENA Auto)))
              THEN (CubicalSubsetICube (-1) THENA Auto)
              THEN Unfold `name-morph-satisfies` -1
              THEN (SubstFor ⌜phi⌝ (-1)⋅ THENA Auto)
              THEN (RWO "fl-morph-0" (-1) THENA Auto)
              THEN (Assert ⌜False⌝⋅ THEN Auto)
              THEN MoveToConcl (-1)
              THEN Fold `not` 0
              THEN Auto)
   ) }

---

Latex:

---

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


By

---

Latex:
(Auto
  THEN  MemTypeCD
            THEN  (Auto
                        THEN  Try  (RepeatFor  2  ((FunExt  THENA  Auto)))
                        THEN  (CubicalSubsetICube  (-1)  THENA  Auto)
                        THEN  Unfold  `name-morph-satisfies`  -1
                        THEN  (SubstFor  \mkleeneopen{}phi\mkleeneclose{}  (-1)\mcdot{}  THENA  Auto)
                        THEN  (RWO  "fl-morph-0"  (-1)  THENA  Auto)
                        THEN  (Assert  \mkleeneopen{}False\mkleeneclose{}\mcdot{}  THEN  Auto)
                        THEN  MoveToConcl  (-1)
                        THEN  Fold  `not`  0
                        THEN  Auto)
  )

---

Home Index