---

Step * of Lemma decidable__l_all

∀[A:Type]. ∀L:A List. ∀[F:{a:A| (a ∈ L)}  ⟶ ℙ]. ((∀k:{a:A| (a ∈ L)} . Dec(F[k])) ⇒ Dec((∀k∈L.F[k])))
BY
{ Extract of Obid: decidable__l_all-proof
  not unfolding  listops
  finishing with xxxTry ((Fold `l-all-decider` 0 THEN Auto))xxx
  normalizes to:
  
  l-all-decider() }

---

Latex:

---

Latex:
\mforall{}[A:Type].  \mforall{}L:A  List.  \mforall{}[F:\{a:A|  (a  \mmember{}  L)\}    {}\mrightarrow{}  \mBbbP{}].  ((\mforall{}k:\{a:A|  (a  \mmember{}  L)\}  .  Dec(F[k]))  {}\mRightarrow{}  Dec((\mforall{}k\mmember{}L.F[k])\000C))


By

---

Latex:
Extract  of  Obid:  decidable\_\_l\_all-proof
not  unfolding    listops
finishing  with  xxxTry  ((Fold  `l-all-decider`  0  THEN  Auto))xxx
normalizes  to:

l-all-decider()

---

Home Index