---

Step * of Lemma decidable__all_fset

∀[T:Type]. ∀eq:EqDecider(T). ∀[P:T ⟶ ℙ]. ((∀x:T. Dec(P[x])) ⇒ (∀s:fset(T). Dec(∀x:T. P[x] supposing x ∈ s)))
BY
{ Auto }

1
.....decidable?..... 
1. [T] : Type
2. eq : EqDecider(T)@i
3. [P] : T ⟶ ℙ
4. ∀x:T. Dec(P[x])@i
5. s : fset(T)@i
⊢ Dec(∀x:T. P[x] supposing x ∈ s)

---

Latex:

---

Latex:
\mforall{}[T:Type]
    \mforall{}eq:EqDecider(T)
        \mforall{}[P:T  {}\mrightarrow{}  \mBbbP{}].  ((\mforall{}x:T.  Dec(P[x]))  {}\mRightarrow{}  (\mforall{}s:fset(T).  Dec(\mforall{}x:T.  P[x]  supposing  x  \mmember{}  s)))


By

---

Latex:
Auto

---

Home Index