---

Step * of Lemma equipollent-nat-list-nat

ℕ List ~ ℕ
BY
{ (InstLemma `equipollent_transitivity` [⌜ℕ List⌝;⌜k:ℕ × (ℕ^k)⌝;⌜ℕ⌝]⋅ THEN Auto) }

1
.....antecedent..... 
k:ℕ × (ℕ^k) ~ ℕ

---

Latex:

---

Latex:
\mBbbN{}  List  \msim{}  \mBbbN{}


By

---

Latex:
(InstLemma  `equipollent\_transitivity`  [\mkleeneopen{}\mBbbN{}  List\mkleeneclose{};\mkleeneopen{}k:\mBbbN{}  \mtimes{}  (\mBbbN{}\^{}k)\mkleeneclose{};\mkleeneopen{}\mBbbN{}\mkleeneclose{}]\mcdot{}  THEN  Auto)

---

Home Index