---

Step * of Lemma face-forall-decomp

No Annotations
∀[H:j⊢]. ∀[phi:{H.𝕀 ⊢ _:𝔽}].  H.𝕀 ⊢ (phi ⇐⇒ (((∀ phi))p ∨ ((phi ∧ (q=0)) ∨ (phi ∧ (q=1)))))
BY
{ (InstLemma `face-forall-implies` [] THEN RepeatFor 2 (ParallelLast') THEN D 0) }

1
1. [H] : CubicalSet{j}
2. [phi] : {H.𝕀 ⊢ _:𝔽}
3. H.𝕀 ⊢ (((∀ phi))p ⇒ phi)
⊢ H.𝕀 ⊢ (phi ⇒ (((∀ phi))p ∨ ((phi ∧ (q=0)) ∨ (phi ∧ (q=1)))))

2
1. [H] : CubicalSet{j}
2. [phi] : {H.𝕀 ⊢ _:𝔽}
3. H.𝕀 ⊢ (((∀ phi))p ⇒ phi)
⊢ H.𝕀 ⊢ ((((∀ phi))p ∨ ((phi ∧ (q=0)) ∨ (phi ∧ (q=1)))) ⇒ phi)

---

Latex:

---

Latex:
No  Annotations
\mforall{}[H:j\mvdash{}].  \mforall{}[phi:\{H.\mBbbI{}  \mvdash{}  \_:\mBbbF{}\}].    H.\mBbbI{}  \mvdash{}  (phi  \mLeftarrow{}{}\mRightarrow{}  (((\mforall{}  phi))p  \mvee{}  ((phi  \mwedge{}  (q=0))  \mvee{}  (phi  \mwedge{}  (q=1)))))


By

---

Latex:
(InstLemma  `face-forall-implies`  []  THEN  RepeatFor  2  (ParallelLast')  THEN  D  0)

---

Home Index