---

Step * 2 2 1 1 1 1 of Lemma Coquand-fan-theorem


1. [T] : Type
2. n : ℕ
3. f : ℕn ⟶ T
4. Surj(ℕn;T;f)
5. y : 0 = 0 ∈ ℤ
6. z2 : T ⟶ wfd-tree(T)
7. ∀b:T. ∀A:n:ℕ ⟶ (ℕn ⟶ T) ⟶ ℙ.
     ((∀n:ℕ. ∀s:ℕn ⟶ T.  ((A n s) ⇒ (∀m:{n...}. ∀t:ℕm ⟶ T.  ((t = s ∈ (ℕn ⟶ T)) ⇒ (A m t)))))
     ⇒ (z2 b|A)
     ⇒ (∃N:ℕ. ∀m:{N...}. ∀as:ℕm ⟶ T.  (A m as)))
8. A : n:ℕ ⟶ (ℕn ⟶ T) ⟶ ℙ
9. ∀n:ℕ. ∀s:ℕn ⟶ T.  ((A n s) ⇒ (∀m:{n...}. ∀t:ℕm ⟶ T.  ((t = s ∈ (ℕn ⟶ T)) ⇒ (A m t))))
10. ∀x:T. (z2 x|A_x)
11. ∀x:T. ∃N:ℕ. ∀m:{N...}. ∀as:ℕm ⟶ T.  (A_x m as)
12. N : x:T ⟶ ℕ
13. ∀x:T. ∀m:{N x...}. ∀as:ℕm ⟶ T.  (A_x m as)
14. 1 ≤ imax-list([1 / map(λi.((N (f i)) + 1);upto(n))])
15. m : ℤ
16. imax-list([1 / map(λi.((N (f i)) + 1);upto(n))]) ≤ m
17. as : ℕm ⟶ T
18. 1 ≤ imax-list([1 / map(λi.((N (f i)) + 1);upto(n))])
⊢ A m as
BY
{ ((With ⌜as 0⌝ (D 4)⋅ THENA Auto)
   THEN ExRepD
   THEN (Subst ⌜(A m as) = (A_f a (m - 1) (λi.(as (i + 1)))) ∈ ℙ⌝ 0⋅
         THENA (RepUR ``predicate-shift seq-append seq-single`` 0
                THEN Auto
                THEN EqCD
                THEN Auto
                THEN Ext
                THEN Reduce 0
                THEN Auto
                THEN RepeatFor 2 (AutoSplit))
         )) }

1
1. [T] : Type
2. n : ℕ
3. f : ℕn ⟶ T
4. y : 0 = 0 ∈ ℤ
5. z2 : T ⟶ wfd-tree(T)
6. ∀b:T. ∀A:n:ℕ ⟶ (ℕn ⟶ T) ⟶ ℙ.
     ((∀n:ℕ. ∀s:ℕn ⟶ T.  ((A n s) ⇒ (∀m:{n...}. ∀t:ℕm ⟶ T.  ((t = s ∈ (ℕn ⟶ T)) ⇒ (A m t)))))
     ⇒ (z2 b|A)
     ⇒ (∃N:ℕ. ∀m:{N...}. ∀as:ℕm ⟶ T.  (A m as)))
7. A : n:ℕ ⟶ (ℕn ⟶ T) ⟶ ℙ
8. ∀n:ℕ. ∀s:ℕn ⟶ T.  ((A n s) ⇒ (∀m:{n...}. ∀t:ℕm ⟶ T.  ((t = s ∈ (ℕn ⟶ T)) ⇒ (A m t))))
9. ∀x:T. (z2 x|A_x)
10. ∀x:T. ∃N:ℕ. ∀m:{N...}. ∀as:ℕm ⟶ T.  (A_x m as)
11. N : x:T ⟶ ℕ
12. ∀x:T. ∀m:{N x...}. ∀as:ℕm ⟶ T.  (A_x m as)
13. 1 ≤ imax-list([1 / map(λi.((N (f i)) + 1);upto(n))])
14. m : ℤ
15. imax-list([1 / map(λi.((N (f i)) + 1);upto(n))]) ≤ m
16. as : ℕm ⟶ T
17. 1 ≤ imax-list([1 / map(λi.((N (f i)) + 1);upto(n))])
18. a : ℕn
19. (f a) = (as 0) ∈ T
⊢ A_f a (m - 1) (λi.(as (i + 1)))

---

Latex:

---

Latex:

1.  [T]  :  Type
2.  n  :  \mBbbN{}
3.  f  :  \mBbbN{}n  {}\mrightarrow{}  T
4.  Surj(\mBbbN{}n;T;f)
5.  y  :  0  =  0
6.  z2  :  T  {}\mrightarrow{}  wfd-tree(T)
7.  \mforall{}b:T.  \mforall{}A:n:\mBbbN{}  {}\mrightarrow{}  (\mBbbN{}n  {}\mrightarrow{}  T)  {}\mrightarrow{}  \mBbbP{}.
          ((\mforall{}n:\mBbbN{}.  \mforall{}s:\mBbbN{}n  {}\mrightarrow{}  T.    ((A  n  s)  {}\mRightarrow{}  (\mforall{}m:\{n...\}.  \mforall{}t:\mBbbN{}m  {}\mrightarrow{}  T.    ((t  =  s)  {}\mRightarrow{}  (A  m  t)))))
          {}\mRightarrow{}  (z2  b|A)
          {}\mRightarrow{}  (\mexists{}N:\mBbbN{}.  \mforall{}m:\{N...\}.  \mforall{}as:\mBbbN{}m  {}\mrightarrow{}  T.    (A  m  as)))
8.  A  :  n:\mBbbN{}  {}\mrightarrow{}  (\mBbbN{}n  {}\mrightarrow{}  T)  {}\mrightarrow{}  \mBbbP{}
9.  \mforall{}n:\mBbbN{}.  \mforall{}s:\mBbbN{}n  {}\mrightarrow{}  T.    ((A  n  s)  {}\mRightarrow{}  (\mforall{}m:\{n...\}.  \mforall{}t:\mBbbN{}m  {}\mrightarrow{}  T.    ((t  =  s)  {}\mRightarrow{}  (A  m  t))))
10.  \mforall{}x:T.  (z2  x|A\_x)
11.  \mforall{}x:T.  \mexists{}N:\mBbbN{}.  \mforall{}m:\{N...\}.  \mforall{}as:\mBbbN{}m  {}\mrightarrow{}  T.    (A\_x  m  as)
12.  N  :  x:T  {}\mrightarrow{}  \mBbbN{}
13.  \mforall{}x:T.  \mforall{}m:\{N  x...\}.  \mforall{}as:\mBbbN{}m  {}\mrightarrow{}  T.    (A\_x  m  as)
14.  1  \mleq{}  imax-list([1  /  map(\mlambda{}i.((N  (f  i))  +  1);upto(n))])
15.  m  :  \mBbbZ{}
16.  imax-list([1  /  map(\mlambda{}i.((N  (f  i))  +  1);upto(n))])  \mleq{}  m
17.  as  :  \mBbbN{}m  {}\mrightarrow{}  T
18.  1  \mleq{}  imax-list([1  /  map(\mlambda{}i.((N  (f  i))  +  1);upto(n))])
\mvdash{}  A  m  as


By

---

Latex:
((With  \mkleeneopen{}as  0\mkleeneclose{}  (D  4)\mcdot{}  THENA  Auto)
  THEN  ExRepD
  THEN  (Subst  \mkleeneopen{}(A  m  as)  =  (A\_f  a  (m  -  1)  (\mlambda{}i.(as  (i  +  1))))\mkleeneclose{}  0\mcdot{}
              THENA  (RepUR  ``predicate-shift  seq-append  seq-single``  0
                            THEN  Auto
                            THEN  EqCD
                            THEN  Auto
                            THEN  Ext
                            THEN  Reduce  0
                            THEN  Auto
                            THEN  RepeatFor  2  (AutoSplit))
              ))

---

Home Index