---

Step * of Lemma Coquand-fan-theorem

∀[T:Type]
  (finite-type(T)
  ⇒ (∀p:wfd-tree(T). ∀A:n:ℕ ⟶ (ℕn ⟶ T) ⟶ ℙ.
        ((∀n:ℕ. ∀s:ℕn ⟶ T.  ((A n s) ⇒ (∀m:{n...}. ∀t:ℕm ⟶ T.  ((t = s ∈ (ℕn ⟶ T)) ⇒ (A m t)))))
        ⇒ (p|A)
        ⇒ (∃N:ℕ. ∀m:{N...}. ∀as:ℕm ⟶ T.  (A m as)))))
BY
{ (RepeatFor 2 ((D 0 THENA Auto))
   THEN Unfold `wfd-tree` 0
   THEN UseWInductionLemma'⋅
   THEN RepeatFor 2 (D -3)
   THEN All (Fold `it`)
   THEN All (Folds ``bfalse btrue``)
   THEN All Reduce
   THEN (RecUnfold `tree-bars` 0 THEN RepUR ``Wsup`` 0 THEN Auto)⋅) }

1
1. [T] : Type
2. finite-type(T)
3. x : 0 = 0 ∈ ℤ
4. f : Void ⟶ W(𝔹;a.if a then Void else T fi )
5. ∀b:Void. ∀A:n:ℕ ⟶ (ℕn ⟶ T) ⟶ ℙ.
     ((∀n:ℕ. ∀s:ℕn ⟶ T.  ((A n s) ⇒ (∀m:{n...}. ∀t:ℕm ⟶ T.  ((t = s ∈ (ℕn ⟶ T)) ⇒ (A m t)))))
     ⇒ (f b|A)
     ⇒ (∃N:ℕ. ∀m:{N...}. ∀as:ℕm ⟶ T.  (A m as)))
6. A : n:ℕ ⟶ (ℕn ⟶ T) ⟶ ℙ
7. ∀n:ℕ. ∀s:ℕn ⟶ T.  ((A n s) ⇒ (∀m:{n...}. ∀t:ℕm ⟶ T.  ((t = s ∈ (ℕn ⟶ T)) ⇒ (A m t))))
8. A 0 (λx.x)
⊢ ∃N:ℕ. ∀m:{N...}. ∀as:ℕm ⟶ T.  (A m as)

2
1. [T] : Type
2. finite-type(T)
3. y : 0 = 0 ∈ ℤ
4. f : T ⟶ W(𝔹;a.if a then Void else T fi )
5. ∀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)))))
     ⇒ (f b|A)
     ⇒ (∃N:ℕ. ∀m:{N...}. ∀as:ℕm ⟶ T.  (A m as)))
6. A : n:ℕ ⟶ (ℕn ⟶ T) ⟶ ℙ
7. ∀n:ℕ. ∀s:ℕn ⟶ T.  ((A n s) ⇒ (∀m:{n...}. ∀t:ℕm ⟶ T.  ((t = s ∈ (ℕn ⟶ T)) ⇒ (A m t))))
8. ∀x:T. (f x|A_x)
⊢ ∃N:ℕ. ∀m:{N...}. ∀as:ℕm ⟶ T.  (A m as)

---

Latex:

---

Latex:
\mforall{}[T:Type]
    (finite-type(T)
    {}\mRightarrow{}  (\mforall{}p:wfd-tree(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{}  (p|A)
                {}\mRightarrow{}  (\mexists{}N:\mBbbN{}.  \mforall{}m:\{N...\}.  \mforall{}as:\mBbbN{}m  {}\mrightarrow{}  T.    (A  m  as)))))


By

---

Latex:
(RepeatFor  2  ((D  0  THENA  Auto))
  THEN  Unfold  `wfd-tree`  0
  THEN  UseWInductionLemma'\mcdot{}
  THEN  RepeatFor  2  (D  -3)
  THEN  All  (Fold  `it`)
  THEN  All  (Folds  ``bfalse  btrue``)
  THEN  All  Reduce
  THEN  (RecUnfold  `tree-bars`  0  THEN  RepUR  ``Wsup``  0  THEN  Auto)\mcdot{})

---

Home Index