---

Step * 2 1 of Lemma finite-iff-listable


1. [T] : Type
2. L : T List
3. no_repeats(T;L)
4. ∀x:T. (x ∈ L)
⊢ T ~ ℕ||L||
BY
{ (BLemma `equipollent-iff-list` THEN Auto) }

---

Latex:

---

Latex:

1.  [T]  :  Type
2.  L  :  T  List
3.  no\_repeats(T;L)
4.  \mforall{}x:T.  (x  \mmember{}  L)
\mvdash{}  T  \msim{}  \mBbbN{}||L||


By

---

Latex:
(BLemma  `equipollent-iff-list`  THEN  Auto)

---

Home Index