---

Step * of Lemma fan-wkl!

∀[T:Type]. ((∃size:ℕ. T ~ ℕsize) ⇒ Fan(T) ⇒ WKL!(T))
BY
{ (InstLemma `alt-bar-sep-wkl!` []
   THEN RepeatFor 2 ((ParallelLast' THENA Auto))
   THEN (D 0 THENA Auto)
   THEN BHyp -2
   THEN Auto
   THEN EAuto 1) }

---

Latex:

---

Latex:
\mforall{}[T:Type].  ((\mexists{}size:\mBbbN{}.  T  \msim{}  \mBbbN{}size)  {}\mRightarrow{}  Fan(T)  {}\mRightarrow{}  WKL!(T))


By

---

Latex:
(InstLemma  `alt-bar-sep-wkl!`  []
  THEN  RepeatFor  2  ((ParallelLast'  THENA  Auto))
  THEN  (D  0  THENA  Auto)
  THEN  BHyp  -2
  THEN  Auto
  THEN  EAuto  1)

---

Home Index