---

Step * 1 1 of Lemma notAC20-ssq


1. T : Type
2. ↓T
3. ∀P:((ℕ ⟶ ℕ) ⟶ ℕ) ⟶ T ⟶ ℙ
     ((∀n:(ℕ ⟶ ℕ) ⟶ ℕ. (↓∃m:T. (P n m))) ⇒ (↓∃f:((ℕ ⟶ ℕ) ⟶ ℕ) ⟶ T. ∀n:(ℕ ⟶ ℕ) ⟶ ℕ. (P n (f n))))
4. P : ((ℕ ⟶ ℕ) ⟶ ℕ) ⟶ ℙ
5. ∀t:(ℕ ⟶ ℕ) ⟶ ℕ. (↓P[t])
⊢ ↓∀t:(ℕ ⟶ ℕ) ⟶ ℕ. P[t]
BY
{ (InstHyp [⌜λf,t. P[f]⌝] (-3)⋅ THENA (RepUR ``so_apply`` 0 THEN Auto)) }

1
1. T : Type
2. T
3. ∀P:((ℕ ⟶ ℕ) ⟶ ℕ) ⟶ T ⟶ ℙ
     ((∀n:(ℕ ⟶ ℕ) ⟶ ℕ. (↓∃m:T. (P n m))) ⇒ (↓∃f:((ℕ ⟶ ℕ) ⟶ ℕ) ⟶ T. ∀n:(ℕ ⟶ ℕ) ⟶ ℕ. (P n (f n))))
4. P : ((ℕ ⟶ ℕ) ⟶ ℕ) ⟶ ℙ
5. ∀t:(ℕ ⟶ ℕ) ⟶ ℕ. (↓P[t])
6. n : (ℕ ⟶ ℕ) ⟶ ℕ
⊢ ↓∃m:T. (P n)

2
1. T : Type
2. ↓T
3. ∀P:((ℕ ⟶ ℕ) ⟶ ℕ) ⟶ T ⟶ ℙ
     ((∀n:(ℕ ⟶ ℕ) ⟶ ℕ. (↓∃m:T. (P n m))) ⇒ (↓∃f:((ℕ ⟶ ℕ) ⟶ ℕ) ⟶ T. ∀n:(ℕ ⟶ ℕ) ⟶ ℕ. (P n (f n))))
4. P : ((ℕ ⟶ ℕ) ⟶ ℕ) ⟶ ℙ
5. ∀t:(ℕ ⟶ ℕ) ⟶ ℕ. (↓P[t])
6. ↓∃f:((ℕ ⟶ ℕ) ⟶ ℕ) ⟶ T. ∀n:(ℕ ⟶ ℕ) ⟶ ℕ. ((λf,t. P[f]) n (f n))
⊢ ↓∀t:(ℕ ⟶ ℕ) ⟶ ℕ. P[t]

---

Latex:

---

Latex:

1.  T  :  Type
2.  \mdownarrow{}T
3.  \mforall{}P:((\mBbbN{}  {}\mrightarrow{}  \mBbbN{})  {}\mrightarrow{}  \mBbbN{})  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbP{}
          ((\mforall{}n:(\mBbbN{}  {}\mrightarrow{}  \mBbbN{})  {}\mrightarrow{}  \mBbbN{}.  (\mdownarrow{}\mexists{}m:T.  (P  n  m)))
          {}\mRightarrow{}  (\mdownarrow{}\mexists{}f:((\mBbbN{}  {}\mrightarrow{}  \mBbbN{})  {}\mrightarrow{}  \mBbbN{})  {}\mrightarrow{}  T.  \mforall{}n:(\mBbbN{}  {}\mrightarrow{}  \mBbbN{})  {}\mrightarrow{}  \mBbbN{}.  (P  n  (f  n))))
4.  P  :  ((\mBbbN{}  {}\mrightarrow{}  \mBbbN{})  {}\mrightarrow{}  \mBbbN{})  {}\mrightarrow{}  \mBbbP{}
5.  \mforall{}t:(\mBbbN{}  {}\mrightarrow{}  \mBbbN{})  {}\mrightarrow{}  \mBbbN{}.  (\mdownarrow{}P[t])
\mvdash{}  \mdownarrow{}\mforall{}t:(\mBbbN{}  {}\mrightarrow{}  \mBbbN{})  {}\mrightarrow{}  \mBbbN{}.  P[t]


By

---

Latex:
(InstHyp  [\mkleeneopen{}\mlambda{}f,t.  P[f]\mkleeneclose{}]  (-3)\mcdot{}  THENA  (RepUR  ``so\_apply``  0  THEN  Auto))

---

Home Index