---

Step * of Lemma l-all-decider_wf

∀[A:Type]
  ∀L:A List. ∀[F:{a:A| (a ∈ L)}  ⟶ ℙ]. ∀dcd:∀k:{a:A| (a ∈ L)} . Dec(F[k]). (l-all-decider() L dcd ∈ Dec((∀k∈L.F[k])))
BY
{ Auto }

1
1. A : Type
2. L : A List
3. F : {a:A| (a ∈ L)}  ⟶ ℙ
4. dcd : ∀k:{a:A| (a ∈ L)} . Dec(F[k])
⊢ l-all-decider() L dcd ∈ Dec((∀k∈L.F[k]))

---

Latex:

---

Latex:
\mforall{}[A:Type]
    \mforall{}L:A  List
        \mforall{}[F:\{a:A|  (a  \mmember{}  L)\}    {}\mrightarrow{}  \mBbbP{}]
            \mforall{}dcd:\mforall{}k:\{a:A|  (a  \mmember{}  L)\}  .  Dec(F[k]).  (l-all-decider()  L  dcd  \mmember{}  Dec((\mforall{}k\mmember{}L.F[k])))


By

---

Latex:
Auto

---

Home Index