---

Step * of Lemma simple_fan_theorem'-ext

∀[X:n:ℕ ⟶ (ℕn ⟶ 𝔹) ⟶ ℙ]
  (∀n:ℕ. ∀s:ℕn ⟶ 𝔹.  Dec(X[n;s])) ⇒ (∃k:ℕ [(∀f:ℕ ⟶ 𝔹. ∃n:ℕk. X[n;f])]) supposing ∀f:ℕ ⟶ 𝔹. (↓∃n:ℕ. X[n;f])
BY
{ Extract of Obid: simple_fan_theorem'
  not unfolding  imax bar_recursion btrue bfalse
  finishing with (Unfold `FAN` 0
                  THEN Try (Fold `bottom` 0)
                  THEN SqequalSqle
                  THEN RepeatFor 3 (SqLeCD)
                  THEN SqReasoning
                  THEN RevHypSubst (-1) 0
                  THEN AutoSplit)
  normalizes to:
  
  λd.FAN(d) }

---

Latex:

---

Latex:
\mforall{}[X:n:\mBbbN{}  {}\mrightarrow{}  (\mBbbN{}n  {}\mrightarrow{}  \mBbbB{})  {}\mrightarrow{}  \mBbbP{}]
    (\mforall{}n:\mBbbN{}.  \mforall{}s:\mBbbN{}n  {}\mrightarrow{}  \mBbbB{}.    Dec(X[n;s]))  {}\mRightarrow{}  (\mexists{}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:
Extract  of  Obid:  simple\_fan\_theorem'
not  unfolding    imax  bar\_recursion  btrue  bfalse
finishing  with  (Unfold  `FAN`  0
                                THEN  Try  (Fold  `bottom`  0)
                                THEN  SqequalSqle
                                THEN  RepeatFor  3  (SqLeCD)
                                THEN  SqReasoning
                                THEN  RevHypSubst  (-1)  0
                                THEN  AutoSplit)
normalizes  to:

\mlambda{}d.FAN(d)

---

Home Index