---

Step * of Lemma equipollent-product-one

∀[A:Type]. (A × ℕ1 ~ A ∧ ℕ1 × A ~ A)
BY
{ TACTIC:Assert ⌜ℕ1 ~ Top⌝⋅ }

1
.....assertion..... 
ℕ1 ~ Top

2
1. ℕ1 ~ Top
⊢ ∀[A:Type]. (A × ℕ1 ~ A ∧ ℕ1 × A ~ A)

---

Latex:

---

Latex:
\mforall{}[A:Type].  (A  \mtimes{}  \mBbbN{}1  \msim{}  A  \mwedge{}  \mBbbN{}1  \mtimes{}  A  \msim{}  A)


By

---

Latex:
TACTIC:Assert  \mkleeneopen{}\mBbbN{}1  \msim{}  Top\mkleeneclose{}\mcdot{}

---

Home Index