---

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

No Annotations
∀[H:j⊢]. ∀[phi:{H.𝕀 ⊢ _:𝔽}]. ∀[K:j⊢]. ∀[tau:K j⟶ H].  K.𝕀 ⊢ ((((∀ phi))tau)p ⇒ (phi)tau+)
BY
{ (Intros
   THEN (Assert tau+ ∈ K.𝕀 j⟶ H.𝕀 BY
               Auto)
   THEN (InstLemma `face-forall-implies` [⌜K⌝;⌜(phi)tau+⌝]⋅ THENA 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+)
⊢ K.𝕀 ⊢ ((((∀ phi))tau)p ⇒ (phi)tau+)

---

Latex:

---

Latex:
No  Annotations
\mforall{}[H:j\mvdash{}].  \mforall{}[phi:\{H.\mBbbI{}  \mvdash{}  \_:\mBbbF{}\}].  \mforall{}[K:j\mvdash{}].  \mforall{}[tau:K  j{}\mrightarrow{}  H].    K.\mBbbI{}  \mvdash{}  ((((\mforall{}  phi))tau)p  {}\mRightarrow{}  (phi)tau+)


By

---

Latex:
(Intros
  THEN  (Assert  tau+  \mmember{}  K.\mBbbI{}  j{}\mrightarrow{}  H.\mBbbI{}  BY
                          Auto)
  THEN  (InstLemma  `face-forall-implies`  [\mkleeneopen{}K\mkleeneclose{};\mkleeneopen{}(phi)tau+\mkleeneclose{}]\mcdot{}  THENA  Auto))

---

Home Index