---

Step * of Lemma decidable__l_all-better-extract

∀[A:Type]. ∀L:A List. ∀[F:{a:A| (a ∈ L)}  ⟶ ℙ]. ((∀k:{a:A| (a ∈ L)} . Dec(F[k])) ⇒ Dec((∀k∈L.F[k])))
BY
{ (InstLemma `decidable__l_all` [] THEN Trivial) }

---

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:
(InstLemma  `decidable\_\_l\_all`  []  THEN  Trivial)

---

Home Index