---

Step * of Lemma twkl!-implies-dfan

∀T:Type. ((∃k:ℕ. T ~ ℕk) ⇒ WKL!(T) ⇒ Fan_d(T))
BY
{ ((Auto THEN D 0 THEN Auto)
   THEN D -1
   THEN (UnfoldTopAb (-1) THEN UnfoldTopAb (-2))
   THEN UnfoldTopAb 0
   THEN RenameVar `s' 4
   THEN Decide ⌜s []⌝⋅
   THEN Auto
   THEN (InstLemma `tree-big-monotone` [⌜T⌝;⌜s⌝]⋅ THENA Auto)) }

1
1. T : Type
2. ∃k:ℕ. T ~ ℕk
3. WKL!(T)
4. s : (T List) ⟶ ℙ
5. ∀t:T List. Dec(s t)
6. ∀f:ℕ ⟶ T. ∃n:ℕ. (s map(f;upto(n)))
7. s []
8. ∀a,b:ℕ.  ((a ≤ b) ⇒ tree-big(T;upwd-closure(T;s);a) ⇒ tree-big(T;upwd-closure(T;s);b))
⊢ ∃k:ℕ. ∀f:ℕ ⟶ T. ∃n:ℕk. (s map(f;upto(n)))

2
1. T : Type
2. ∃k:ℕ. T ~ ℕk
3. WKL!(T)
4. s : (T List) ⟶ ℙ
5. ∀t:T List. Dec(s t)
6. ∀f:ℕ ⟶ T. ∃n:ℕ. (s map(f;upto(n)))
7. ¬(s [])
8. ∀a,b:ℕ.  ((a ≤ b) ⇒ tree-big(T;upwd-closure(T;s);a) ⇒ tree-big(T;upwd-closure(T;s);b))
⊢ ∃k:ℕ. ∀f:ℕ ⟶ T. ∃n:ℕk. (s map(f;upto(n)))

---

Latex:

---

Latex:
\mforall{}T:Type.  ((\mexists{}k:\mBbbN{}.  T  \msim{}  \mBbbN{}k)  {}\mRightarrow{}  WKL!(T)  {}\mRightarrow{}  Fan\_d(T))


By

---

Latex:
((Auto  THEN  D  0  THEN  Auto)
  THEN  D  -1
  THEN  (UnfoldTopAb  (-1)  THEN  UnfoldTopAb  (-2))
  THEN  UnfoldTopAb  0
  THEN  RenameVar  `s'  4
  THEN  Decide  \mkleeneopen{}s  []\mkleeneclose{}\mcdot{}
  THEN  Auto
  THEN  (InstLemma  `tree-big-monotone`  [\mkleeneopen{}T\mkleeneclose{};\mkleeneopen{}s\mkleeneclose{}]\mcdot{}  THENA  Auto))

---

Home Index