---

Step * of Lemma face-forall-1

No Annotations
∀[Gamma:j⊢]. ∀[phi:{Gamma.𝕀 ⊢ _:𝔽}].  (Gamma ⊢ ∀ phi) = 1(𝔽) ∈ {Gamma ⊢ _:𝔽} supposing phi = 1(𝔽) ∈ {Gamma.𝕀 ⊢ _:𝔽}
BY
{ (Auto THEN (RWO "-1" 0 THENA Auto) THEN All Thin) }

1
1. Gamma : CubicalSet{j}
⊢ (Gamma ⊢ ∀ 1(𝔽)) = 1(𝔽) ∈ {Gamma ⊢ _:𝔽}

---

Latex:

---

Latex:
No  Annotations
\mforall{}[Gamma:j\mvdash{}].  \mforall{}[phi:\{Gamma.\mBbbI{}  \mvdash{}  \_:\mBbbF{}\}].    (Gamma  \mvdash{}  \mforall{}  phi)  =  1(\mBbbF{})  supposing  phi  =  1(\mBbbF{})


By

---

Latex:
(Auto  THEN  (RWO  "-1"  0  THENA  Auto)  THEN  All  Thin)

---

Home Index