---

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


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)
9. x : T
10. ∀A:n:ℕ ⟶ (ℕn ⟶ T) ⟶ ℙ
      ((∀n:ℕ. ∀s:ℕn ⟶ T.  ((A n s) ⇒ (∀m:{n...}. ∀t:ℕm ⟶ T.  ((t = s ∈ (ℕn ⟶ T)) ⇒ (A m t)))))
      ⇒ (f x|A)
      ⇒ (∃N:ℕ. ∀m:{N...}. ∀as:ℕm ⟶ T.  (A m as)))
11. n : ℕ
12. s : ℕn ⟶ T
13. A (n + 1) seq-append(1;n;seq-single(x);s)
14. m : {n...}
15. t : ℕm ⟶ T
16. t = s ∈ (ℕn ⟶ T)
⊢ A (m + 1) seq-append(1;m;seq-single(x);t)
BY
{ ((InstHyp [⌜n + 1⌝;⌜seq-append(1;n;seq-single(x);s)⌝] 7⋅ THENA Auto) THEN BHyp -1  THEN Auto) }

1
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)
9. x : T
10. ∀A:n:ℕ ⟶ (ℕn ⟶ T) ⟶ ℙ
      ((∀n:ℕ. ∀s:ℕn ⟶ T.  ((A n s) ⇒ (∀m:{n...}. ∀t:ℕm ⟶ T.  ((t = s ∈ (ℕn ⟶ T)) ⇒ (A m t)))))
      ⇒ (f x|A)
      ⇒ (∃N:ℕ. ∀m:{N...}. ∀as:ℕm ⟶ T.  (A m as)))
11. n : ℕ
12. s : ℕn ⟶ T
13. A (n + 1) seq-append(1;n;seq-single(x);s)
14. m : {n...}
15. t : ℕm ⟶ T
16. t = s ∈ (ℕn ⟶ T)
17. ∀m:{n + 1...}. ∀t:ℕm ⟶ T.  ((t = seq-append(1;n;seq-single(x);s) ∈ (ℕn + 1 ⟶ T)) ⇒ (A m t))
⊢ seq-append(1;m;seq-single(x);t) = seq-append(1;n;seq-single(x);s) ∈ (ℕn + 1 ⟶ T)

---

Latex:

---

Latex:

1.  [T]  :  Type
2.  finite-type(T)
3.  y  :  0  =  0
4.  f  :  T  {}\mrightarrow{}  W(\mBbbB{};a.if  a  then  Void  else  T  fi  )
5.  \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{}  (f  b|A)
          {}\mRightarrow{}  (\mexists{}N:\mBbbN{}.  \mforall{}m:\{N...\}.  \mforall{}as:\mBbbN{}m  {}\mrightarrow{}  T.    (A  m  as)))
6.  A  :  n:\mBbbN{}  {}\mrightarrow{}  (\mBbbN{}n  {}\mrightarrow{}  T)  {}\mrightarrow{}  \mBbbP{}
7.  \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))))
8.  \mforall{}x:T.  (f  x|A\_x)
9.  x  :  T
10.  \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{}  (f  x|A)
            {}\mRightarrow{}  (\mexists{}N:\mBbbN{}.  \mforall{}m:\{N...\}.  \mforall{}as:\mBbbN{}m  {}\mrightarrow{}  T.    (A  m  as)))
11.  n  :  \mBbbN{}
12.  s  :  \mBbbN{}n  {}\mrightarrow{}  T
13.  A  (n  +  1)  seq-append(1;n;seq-single(x);s)
14.  m  :  \{n...\}
15.  t  :  \mBbbN{}m  {}\mrightarrow{}  T
16.  t  =  s
\mvdash{}  A  (m  +  1)  seq-append(1;m;seq-single(x);t)


By

---

Latex:
((InstHyp  [\mkleeneopen{}n  +  1\mkleeneclose{};\mkleeneopen{}seq-append(1;n;seq-single(x);s)\mkleeneclose{}]  7\mcdot{}  THENA  Auto)  THEN  BHyp  -1    THEN  Auto)

---

Home Index