---

Step * of Lemma decidable__l_all-proof

∀[A:Type]. ∀L:A List. ∀[F:{a:A| (a ∈ L)}  ⟶ ℙ]. ((∀k:{a:A| (a ∈ L)} . Dec(F[k])) ⇒ Dec((∀k∈L.F[k])))
BY
{ (Auto
   THEN Unfold `l_all` 0
   THEN ProveDecidable1
   THEN Try (Complete (Auto))
   THEN Try (((MemTypeCD THEN Auto) THEN With ⌜i⌝ (D 0)⋅ THEN Auto))) }

---

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:
(Auto
  THEN  Unfold  `l\_all`  0
  THEN  ProveDecidable1
  THEN  Try  (Complete  (Auto))
  THEN  Try  (((MemTypeCD  THEN  Auto)  THEN  With  \mkleeneopen{}i\mkleeneclose{}  (D  0)\mcdot{}  THEN  Auto)))

---

Home Index