---

Step * of Lemma cubical-sigma-normalize

∀[X,A,B:Top].  (Σ A B ~ Σ A B)
BY
{ (Intros THEN Computation) }

---

Latex:

---

Latex:
\mforall{}[X,A,B:Top].    (\mSigma{}  A  B  \msim{}  \mSigma{}  A  B)


By

---

Latex:
(Intros  THEN  Computation)

---

Home Index