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