---

Step * of Lemma cc-fst-comp-csm-m-term

No Annotations
∀[H:j⊢]. ∀[phi:{H ⊢ _:𝔽}].  (((phi)p)m = ((phi)p)p ∈ {H.𝕀.𝕀 ⊢ _:𝔽})
BY
{ Auto }

1
1. H : CubicalSet{j}
2. phi : {H ⊢ _:𝔽}
⊢ ((phi)p)m = ((phi)p)p ∈ {H.𝕀.𝕀 ⊢ _:𝔽}

---

Latex:

---

Latex:
No  Annotations
\mforall{}[H:j\mvdash{}].  \mforall{}[phi:\{H  \mvdash{}  \_:\mBbbF{}\}].    (((phi)p)m  =  ((phi)p)p)


By

---

Latex:
Auto

---

Home Index