---

Step * 1 1 of Lemma finite-type-iff-list


1. [T] : Type
2. n : ℕ@i
3. ∃f:ℕn ⟶ T. Surj(ℕn;T;f)@i
4. ∃L:T List. ((||L|| = n ∈ ℤ) ∧ (∀x:T. (x ∈ L)))
⊢ ∃L:T List. ∀x:T. (x ∈ L)
BY
{ (ParallelLast THEN Auto) }

---

Latex:

---

Latex:

1.  [T]  :  Type
2.  n  :  \mBbbN{}@i
3.  \mexists{}f:\mBbbN{}n  {}\mrightarrow{}  T.  Surj(\mBbbN{}n;T;f)@i
4.  \mexists{}L:T  List.  ((||L||  =  n)  \mwedge{}  (\mforall{}x:T.  (x  \mmember{}  L)))
\mvdash{}  \mexists{}L:T  List.  \mforall{}x:T.  (x  \mmember{}  L)


By

---

Latex:
(ParallelLast  THEN  Auto)

---

Home Index