---

Step * of Lemma simple_more_general_fan_theorem-ext

∀[T:ℕ ⟶ Type]
  (∀i:ℕ. Bounded(T[i]))
  ⇒ (∀[X:n:ℕ ⟶ (i:ℕn ⟶ T[i]) ⟶ ℙ]
        (∀n:ℕ. ∀s:i:ℕn ⟶ T[i].  Dec(X[n;s])) ⇒ (∃k:ℕ [(∀f:i:ℕ ⟶ T[i]. ∃n:ℕk. X[n;f])]) 
        supposing ∀f:i:ℕ ⟶ T[i]. (↓∃n:ℕ. X[n;f])) 
  supposing ∀i:ℕ. T[i]
BY
{ Extract of Obid: simple_more_general_fan_theorem
  not unfolding  pi1 int_seg_decide bar_recursion
  finishing with (Unfold `genFAN` 0
                  THEN RepeatFor 4 (EqCD)
                  THEN Try (Trivial)
                  THEN Try (Fold `bottom` 0)
                  THEN SqReasoning)
  normalizes to:
  
  λmax,d. genFAN(max;d) }

---

Latex:

---

Latex:
\mforall{}[T:\mBbbN{}  {}\mrightarrow{}  Type]
    (\mforall{}i:\mBbbN{}.  Bounded(T[i]))
    {}\mRightarrow{}  (\mforall{}[X:n:\mBbbN{}  {}\mrightarrow{}  (i:\mBbbN{}n  {}\mrightarrow{}  T[i])  {}\mrightarrow{}  \mBbbP{}]
                (\mforall{}n:\mBbbN{}.  \mforall{}s:i:\mBbbN{}n  {}\mrightarrow{}  T[i].    Dec(X[n;s]))  {}\mRightarrow{}  (\mexists{}k:\mBbbN{}  [(\mforall{}f:i:\mBbbN{}  {}\mrightarrow{}  T[i].  \mexists{}n:\mBbbN{}k.  X[n;f])]) 
                supposing  \mforall{}f:i:\mBbbN{}  {}\mrightarrow{}  T[i].  (\mdownarrow{}\mexists{}n:\mBbbN{}.  X[n;f])) 
    supposing  \mforall{}i:\mBbbN{}.  T[i]


By

---

Latex:
Extract  of  Obid:  simple\_more\_general\_fan\_theorem
not  unfolding    pi1  int\_seg\_decide  bar\_recursion
finishing  with  (Unfold  `genFAN`  0
                                THEN  RepeatFor  4  (EqCD)
                                THEN  Try  (Trivial)
                                THEN  Try  (Fold  `bottom`  0)
                                THEN  SqReasoning)
normalizes  to:

\mlambda{}max,d.  genFAN(max;d)

---

Home Index