---

Step * 1 of Lemma face-forall-decomp


1. [H] : CubicalSet{j}
2. [phi] : {H.𝕀 ⊢ _:𝔽}
3. H.𝕀 ⊢ (((∀ phi))p ⇒ phi)
⊢ H.𝕀 ⊢ (phi ⇒ (((∀ phi))p ∨ ((phi ∧ (q=0)) ∨ (phi ∧ (q=1)))))
BY
{ ((Assert p ∈ H.𝕀 j⟶ H BY
          Auto)
   THEN D 0
   THEN Auto
   THEN RepUR ``cube-context-adjoin`` -2
   THEN D -2
   THEN (RWO "interval-type-at" (-2) THENA Auto)
   THEN RepUR ``interval-presheaf`` -2
   THEN RenameVar `x' (-2)
   THEN (InstLemma `nc-p_wf` [⌜I⌝;⌜new-name(I)⌝;⌜x⌝]⋅ THENA Auto)
   THEN (Assert <new-name(I)> ∈ 𝕀(s(alpha)) BY
               ((RWO "interval-type-at" 0 THENA Auto) THEN RepUR ``interval-presheaf`` 0 THEN Auto))) }

1
1. H : CubicalSet{j}
2. phi : {H.𝕀 ⊢ _:𝔽}
3. H.𝕀 ⊢ (((∀ phi))p ⇒ phi)
4. p ∈ H.𝕀 j⟶ H
5. I : fset(ℕ)
6. alpha : H(I)
7. x : Point(dM(I))
8. phi(<alpha, x>) = 1 ∈ Point(face_lattice(I))
9. (new-name(I)/x) ∈ I ⟶ I+new-name(I)
10. <new-name(I)> ∈ 𝕀(s(alpha))
⊢ (((∀ phi))p ∨ ((phi ∧ (q=0)) ∨ (phi ∧ (q=1))))(<alpha, x>) = 1 ∈ Point(face_lattice(I))

---

Latex:

---

Latex:

1.  [H]  :  CubicalSet\{j\}
2.  [phi]  :  \{H.\mBbbI{}  \mvdash{}  \_:\mBbbF{}\}
3.  H.\mBbbI{}  \mvdash{}  (((\mforall{}  phi))p  {}\mRightarrow{}  phi)
\mvdash{}  H.\mBbbI{}  \mvdash{}  (phi  {}\mRightarrow{}  (((\mforall{}  phi))p  \mvee{}  ((phi  \mwedge{}  (q=0))  \mvee{}  (phi  \mwedge{}  (q=1)))))


By

---

Latex:
((Assert  p  \mmember{}  H.\mBbbI{}  j{}\mrightarrow{}  H  BY
                Auto)
  THEN  D  0
  THEN  Auto
  THEN  RepUR  ``cube-context-adjoin``  -2
  THEN  D  -2
  THEN  (RWO  "interval-type-at"  (-2)  THENA  Auto)
  THEN  RepUR  ``interval-presheaf``  -2
  THEN  RenameVar  `x'  (-2)
  THEN  (InstLemma  `nc-p\_wf`  [\mkleeneopen{}I\mkleeneclose{};\mkleeneopen{}new-name(I)\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (Assert  <new-name(I)>  \mmember{}  \mBbbI{}(s(alpha))  BY
                          ((RWO  "interval-type-at"  0  THENA  Auto)  THEN  RepUR  ``interval-presheaf``  0  THEN  Auto)))

---

Home Index