---

Step * 2 of Lemma finite-iff-listable


1. [T] : Type
2. ∃L:T List. (no_repeats(T;L) ∧ (∀x:T. (x ∈ L)))
⊢ finite(T)
BY
{ (ExRepD THEN D 0 With ⌜||L||⌝  THEN Auto) }

1
1. [T] : Type
2. L : T List
3. no_repeats(T;L)
4. ∀x:T. (x ∈ L)
⊢ T ~ ℕ||L||

---

Latex:

---

Latex:

1.  [T]  :  Type
2.  \mexists{}L:T  List.  (no\_repeats(T;L)  \mwedge{}  (\mforall{}x:T.  (x  \mmember{}  L)))
\mvdash{}  finite(T)


By

---

Latex:
(ExRepD  THEN  D  0  With  \mkleeneopen{}||L||\mkleeneclose{}    THEN  Auto)

---

Home Index