---

Step * of Lemma partial-term-1_wf

No Annotations
∀[H:j⊢]. ∀[A:{H.𝕀 ⊢ _}]. ∀[phi:{H ⊢ _:𝔽}]. ∀[u:{H.𝕀, (phi)p ⊢ _:A}].  (u[1] ∈ {H, phi ⊢ _:(A)[1(𝕀)]})
BY
{ (Intros THEN Assert ⌜((phi)p)[1(𝕀)] ∈ {H ⊢ _:𝔽}⌝⋅) }

1
.....assertion..... 
1. [H] : CubicalSet{j}
2. [A] : {H.𝕀 ⊢ _}
3. [phi] : {H ⊢ _:𝔽}
4. [u] : {H.𝕀, (phi)p ⊢ _:A}
⊢ ((phi)p)[1(𝕀)] ∈ {H ⊢ _:𝔽}

2
1. [H] : CubicalSet{j}
2. [A] : {H.𝕀 ⊢ _}
3. [phi] : {H ⊢ _:𝔽}
4. [u] : {H.𝕀, (phi)p ⊢ _:A}
5. ((phi)p)[1(𝕀)] ∈ {H ⊢ _:𝔽}
⊢ u[1] ∈ {H, phi ⊢ _:(A)[1(𝕀)]}

---

Latex:

---

Latex:
No  Annotations
\mforall{}[H:j\mvdash{}].  \mforall{}[A:\{H.\mBbbI{}  \mvdash{}  \_\}].  \mforall{}[phi:\{H  \mvdash{}  \_:\mBbbF{}\}].  \mforall{}[u:\{H.\mBbbI{},  (phi)p  \mvdash{}  \_:A\}].
    (u[1]  \mmember{}  \{H,  phi  \mvdash{}  \_:(A)[1(\mBbbI{})]\})


By

---

Latex:
(Intros  THEN  Assert  \mkleeneopen{}((phi)p)[1(\mBbbI{})]  \mmember{}  \{H  \mvdash{}  \_:\mBbbF{}\}\mkleeneclose{}\mcdot{})

---

Home Index