---

Step * 1 of Lemma face-forall-implies-csm+


1. [H] : CubicalSet{j}
2. [phi] : {H.𝕀 ⊢ _:𝔽}
3. [K] : CubicalSet{j}
4. [tau] : K j⟶ H
5. tau+ ∈ K.𝕀 j⟶ H.𝕀
6. K.𝕀 ⊢ (((∀ (phi)tau+))p ⇒ (phi)tau+)
⊢ K.𝕀 ⊢ ((((∀ phi))tau)p ⇒ (phi)tau+)
BY
{ (Assert p ∈ K.𝕀 j⟶ K BY
         Auto) }

1
1. [H] : CubicalSet{j}
2. [phi] : {H.𝕀 ⊢ _:𝔽}
3. [K] : CubicalSet{j}
4. [tau] : K j⟶ H
5. tau+ ∈ K.𝕀 j⟶ H.𝕀
6. K.𝕀 ⊢ (((∀ (phi)tau+))p ⇒ (phi)tau+)
7. p ∈ K.𝕀 j⟶ K
⊢ K.𝕀 ⊢ ((((∀ phi))tau)p ⇒ (phi)tau+)

---

Latex:

---

Latex:

1.  [H]  :  CubicalSet\{j\}
2.  [phi]  :  \{H.\mBbbI{}  \mvdash{}  \_:\mBbbF{}\}
3.  [K]  :  CubicalSet\{j\}
4.  [tau]  :  K  j{}\mrightarrow{}  H
5.  tau+  \mmember{}  K.\mBbbI{}  j{}\mrightarrow{}  H.\mBbbI{}
6.  K.\mBbbI{}  \mvdash{}  (((\mforall{}  (phi)tau+))p  {}\mRightarrow{}  (phi)tau+)
\mvdash{}  K.\mBbbI{}  \mvdash{}  ((((\mforall{}  phi))tau)p  {}\mRightarrow{}  (phi)tau+)


By

---

Latex:
(Assert  p  \mmember{}  K.\mBbbI{}  j{}\mrightarrow{}  K  BY
              Auto)

---

Home Index