---

Step * 1 2 1 of Lemma notAC20


1. T : Type@i'
2. ⇃T@i
3. ∀P:((ℕ ⟶ ℕ) ⟶ ℕ) ⟶ T ⟶ ℙ
     ((∀n:(ℕ ⟶ ℕ) ⟶ ℕ. ⇃∃m:T. (P n m)) ⇒ ⇃∃f:((ℕ ⟶ ℕ) ⟶ ℕ) ⟶ T. ∀n:(ℕ ⟶ ℕ) ⟶ ℕ. (P n (f n)))@i'
4. P : ((ℕ ⟶ ℕ) ⟶ ℕ) ⟶ ℙ@i'
5. ⇃(∀t:(ℕ ⟶ ℕ) ⟶ ℕ. P[t])@i
6. t : (ℕ ⟶ ℕ) ⟶ ℕ@i
⊢ ⇃(P[t])
BY
{ (Assert ⌜(∀t:(ℕ ⟶ ℕ) ⟶ ℕ. P[t]) ⇒ P[t]⌝⋅ THEN Auto) }

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

---

Latex:

---

Latex:

1.  T  :  Type@i'
2.  \00D9T@i
3.  \mforall{}P:((\mBbbN{}  {}\mrightarrow{}  \mBbbN{})  {}\mrightarrow{}  \mBbbN{})  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbP{}
          ((\mforall{}n:(\mBbbN{}  {}\mrightarrow{}  \mBbbN{})  {}\mrightarrow{}  \mBbbN{}.  \00D9\mexists{}m:T.  (P  n  m))
          {}\mRightarrow{}  \00D9\mexists{}f:((\mBbbN{}  {}\mrightarrow{}  \mBbbN{})  {}\mrightarrow{}  \mBbbN{})  {}\mrightarrow{}  T.  \mforall{}n:(\mBbbN{}  {}\mrightarrow{}  \mBbbN{})  {}\mrightarrow{}  \mBbbN{}.  (P  n  (f  n)))@i'
4.  P  :  ((\mBbbN{}  {}\mrightarrow{}  \mBbbN{})  {}\mrightarrow{}  \mBbbN{})  {}\mrightarrow{}  \mBbbP{}@i'
5.  \00D9(\mforall{}t:(\mBbbN{}  {}\mrightarrow{}  \mBbbN{})  {}\mrightarrow{}  \mBbbN{}.  P[t])@i
6.  t  :  (\mBbbN{}  {}\mrightarrow{}  \mBbbN{})  {}\mrightarrow{}  \mBbbN{}@i
\mvdash{}  \00D9(P[t])


By

---

Latex:
(Assert  \mkleeneopen{}(\mforall{}t:(\mBbbN{}  {}\mrightarrow{}  \mBbbN{})  {}\mrightarrow{}  \mBbbN{}.  P[t])  {}\mRightarrow{}  P[t]\mkleeneclose{}\mcdot{}  THEN  Auto)

---

Home Index