---

Step * of Lemma genFAN_wf

∀[T:ℕ ⟶ Type]
  ∀[max:∀i:ℕ. Bounded(T[i])]. ∀[X:n:ℕ ⟶ (i:ℕn ⟶ T[i]) ⟶ ℙ].
    ∀[d:∀n:ℕ. ∀s:i:ℕn ⟶ T[i].  Dec(X[n;s])]. (genFAN(max;d) ∈ {k:ℕ| ∀f:i:ℕ ⟶ T[i]. ∃n:ℕk. X[n;f]} ) 
    supposing ∀f:i:ℕ ⟶ T[i]. (↓∃n:ℕ. X[n;f]) 
  supposing ∀i:ℕ. T[i]
BY
{ (Auto
   THEN (Subst' genFAN(max;d) ~ TERMOF{simple_more_general_fan_theorem-ext:o, \\v:l, i:l} max d 0 THENA Computation)
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[T:\mBbbN{}  {}\mrightarrow{}  Type]
    \mforall{}[max:\mforall{}i:\mBbbN{}.  Bounded(T[i])].  \mforall{}[X:n:\mBbbN{}  {}\mrightarrow{}  (i:\mBbbN{}n  {}\mrightarrow{}  T[i])  {}\mrightarrow{}  \mBbbP{}].
        \mforall{}[d:\mforall{}n:\mBbbN{}.  \mforall{}s:i:\mBbbN{}n  {}\mrightarrow{}  T[i].    Dec(X[n;s])].  (genFAN(max;d)  \mmember{}  \{k:\mBbbN{}|  \mforall{}f:i:\mBbbN{}  {}\mrightarrow{}  T[i].  \mexists{}n:\mBbbN{}k.  X[n;f]\}  \000C) 
        supposing  \mforall{}f:i:\mBbbN{}  {}\mrightarrow{}  T[i].  (\mdownarrow{}\mexists{}n:\mBbbN{}.  X[n;f]) 
    supposing  \mforall{}i:\mBbbN{}.  T[i]


By

---

Latex:
(Auto
  THEN  (Subst'  genFAN(max;d)  \msim{}  TERMOF\{simple\_more\_general\_fan\_theorem-ext:o,  \mbackslash{}\mbackslash{}v:l,  i:l\}  max  d  0
              THENA  Computation
              )
  THEN  Auto)

---

Home Index