---

Step * of Lemma FAN_wf

∀[X:n:ℕ ⟶ (ℕn ⟶ 𝔹) ⟶ ℙ]
  ∀[d:∀n:ℕ. ∀s:ℕn ⟶ 𝔹.  Dec(X[n;s])]. (FAN(d) ∈ {k:ℕ| ∀f:ℕ ⟶ 𝔹. ∃n:ℕk. X[n;f]} ) supposing ∀f:ℕ ⟶ 𝔹. (↓∃n:ℕ. X[n;f])
BY
{ ((Intros THEN Fold `sq_exists` 0)
   THEN (Subst' FAN(d) ~ TERMOF{simple_fan_theorem'-ext:o, \\v:l, i:l} d 0 THENM Auto)
   THEN Computation⋅) }

---

Latex:

---

Latex:
\mforall{}[X:n:\mBbbN{}  {}\mrightarrow{}  (\mBbbN{}n  {}\mrightarrow{}  \mBbbB{})  {}\mrightarrow{}  \mBbbP{}]
    \mforall{}[d:\mforall{}n:\mBbbN{}.  \mforall{}s:\mBbbN{}n  {}\mrightarrow{}  \mBbbB{}.    Dec(X[n;s])].  (FAN(d)  \mmember{}  \{k:\mBbbN{}|  \mforall{}f:\mBbbN{}  {}\mrightarrow{}  \mBbbB{}.  \mexists{}n:\mBbbN{}k.  X[n;f]\}  ) 
    supposing  \mforall{}f:\mBbbN{}  {}\mrightarrow{}  \mBbbB{}.  (\mdownarrow{}\mexists{}n:\mBbbN{}.  X[n;f])


By

---

Latex:
((Intros  THEN  Fold  `sq\_exists`  0)
  THEN  (Subst'  FAN(d)  \msim{}  TERMOF\{simple\_fan\_theorem'-ext:o,  \mbackslash{}\mbackslash{}v:l,  i:l\}  d  0  THENM  Auto)
  THEN  Computation\mcdot{})

---

Home Index