---

Step * 1 of Lemma equipollent-nat-list-nat

.....antecedent..... 
k:ℕ × (ℕ^k) ~ ℕ
BY
{ (BLemma `equipollent_inversion` THEN Auto) }

---

Latex:

---

Latex:
.....antecedent..... 
k:\mBbbN{}  \mtimes{}  (\mBbbN{}\^{}k)  \msim{}  \mBbbN{}


By

---

Latex:
(BLemma  `equipollent\_inversion`  THEN  Auto)

---

Home Index