---

Step * of Lemma decidable__all_length

∀[T:Type]. ∀[P:(T List) ⟶ ℙ].
  ((∀L:T List. Dec(P[L])) ⇒ (∃k:ℕ. T ~ ℕk) ⇒ (∀n:ℕ. Dec(∀L:T List. ((||L|| = n ∈ ℤ) ⇒ P[L]))))
BY
{ (Auto
   THEN ExRepD
   THEN (InstLemma  `decidable__all_finite` [⌜{L:T List| ||L|| = n ∈ ℤ} ⌝;⌜k^n⌝;⌜P⌝]⋅
         THENA (Auto THEN BLemma `equipollent-list` THEN Auto)
         )
   THEN RepeatFor 2 (ParallelLast)
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[P:(T  List)  {}\mrightarrow{}  \mBbbP{}].
    ((\mforall{}L:T  List.  Dec(P[L]))  {}\mRightarrow{}  (\mexists{}k:\mBbbN{}.  T  \msim{}  \mBbbN{}k)  {}\mRightarrow{}  (\mforall{}n:\mBbbN{}.  Dec(\mforall{}L:T  List.  ((||L||  =  n)  {}\mRightarrow{}  P[L]))))


By

---

Latex:
(Auto
  THEN  ExRepD
  THEN  (InstLemma    `decidable\_\_all\_finite`  [\mkleeneopen{}\{L:T  List|  ||L||  =  n\}  \mkleeneclose{};\mkleeneopen{}k\^{}n\mkleeneclose{};\mkleeneopen{}P\mkleeneclose{}]\mcdot{}
              THENA  (Auto  THEN  BLemma  `equipollent-list`  THEN  Auto)
              )
  THEN  RepeatFor  2  (ParallelLast)
  THEN  Auto)

---

Home Index