---

Step * of Lemma simple-finite-cantor-decider_wf

∀[T:Type]. ∀[R:T ⟶ ℙ]. ∀[dcdr:∀x:T. Dec(R[x])]. ∀[n:ℕ]. ∀[F:(ℕn ⟶ 𝔹) ⟶ T].
  (FiniteCantorDecide(dcdr;n;F) ∈ Dec(∃f:ℕn ⟶ 𝔹. R[F f]))
BY
{ (Auto
   THEN Assert ⌜λdcdr,n,F. FiniteCantorDecide(dcdr;n;F) ∈ ∀[T:Type]. ∀[R:T ⟶ ℙ].
                                                   ((∀x:T. Dec(R[x]))
                                                   ⇒ (∀n:ℕ. ∀F:(ℕn ⟶ 𝔹) ⟶ T.  Dec(∃f:ℕn ⟶ 𝔹. R[F f])))⌝⋅
   ) }

1
.....assertion..... 
1. T : Type
2. R : T ⟶ ℙ
3. dcdr : ∀x:T. Dec(R[x])
4. n : ℕ
5. F : (ℕn ⟶ 𝔹) ⟶ T
⊢ λdcdr,n,F. FiniteCantorDecide(dcdr;n;F) ∈ ∀[T:Type]. ∀[R:T ⟶ ℙ].
                                     ((∀x:T. Dec(R[x])) ⇒ (∀n:ℕ. ∀F:(ℕn ⟶ 𝔹) ⟶ T.  Dec(∃f:ℕn ⟶ 𝔹. R[F f])))

2
1. T : Type
2. R : T ⟶ ℙ
3. dcdr : ∀x:T. Dec(R[x])
4. n : ℕ
5. F : (ℕn ⟶ 𝔹) ⟶ T
6. λdcdr,n,F. FiniteCantorDecide(dcdr;n;F) ∈ ∀[T:Type]. ∀[R:T ⟶ ℙ].
                                      ((∀x:T. Dec(R[x])) ⇒ (∀n:ℕ. ∀F:(ℕn ⟶ 𝔹) ⟶ T.  Dec(∃f:ℕn ⟶ 𝔹. R[F f])))
⊢ FiniteCantorDecide(dcdr;n;F) ∈ Dec(∃f:ℕn ⟶ 𝔹. R[F f])

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[R:T  {}\mrightarrow{}  \mBbbP{}].  \mforall{}[dcdr:\mforall{}x:T.  Dec(R[x])].  \mforall{}[n:\mBbbN{}].  \mforall{}[F:(\mBbbN{}n  {}\mrightarrow{}  \mBbbB{})  {}\mrightarrow{}  T].
    (FiniteCantorDecide(dcdr;n;F)  \mmember{}  Dec(\mexists{}f:\mBbbN{}n  {}\mrightarrow{}  \mBbbB{}.  R[F  f]))


By

---

Latex:
(Auto
  THEN  Assert  \mkleeneopen{}\mlambda{}dcdr,n,F.  FiniteCantorDecide(dcdr;n;F)  \mmember{}  \mforall{}[T:Type].  \mforall{}[R:T  {}\mrightarrow{}  \mBbbP{}].
                                                                                                  ((\mforall{}x:T.  Dec(R[x]))
                                                                                                  {}\mRightarrow{}  (\mforall{}n:\mBbbN{}.  \mforall{}F:(\mBbbN{}n  {}\mrightarrow{}  \mBbbB{})  {}\mrightarrow{}  T.
                                                                                                              Dec(\mexists{}f:\mBbbN{}n  {}\mrightarrow{}  \mBbbB{}.  R[F  f])))\mkleeneclose{}\mcdot{}
  )

---

Home Index