---

Step * of Lemma sigma-unelim-p-term

∀[t:Top]. (((t)p)SigmaUnElim ~ ((t)p)p)
BY
{ PresheafMLTTInstance Obid: ps-sigma-unelim-p-term⋅ }

---

Latex:

---

Latex:
\mforall{}[t:Top].  (((t)p)SigmaUnElim  \msim{}  ((t)p)p)


By

---

Latex:
PresheafMLTTInstance  Obid:  ps-sigma-unelim-p-term\mcdot{}

---

Home Index