---

Step * 1 of Lemma decidable__squash_exists_fset


1. [T] : Type
2. [P] : T ⟶ ℙ
3. eq : EqDecider(T)
4. s : fset(T)
5. d : ∀x:T. Dec(P[x])
6. ∀x:T. (isl(d x) ∈ 𝔹)
7. ∀x:T. (↑isl(d x) ⇐⇒ P[x])
8. ¬↑fset-null({x ∈ s | isl(d x)})
⊢ ↓∃x:T. (x ∈ s ∧ P[x])
BY
{ (MoveToConcl (-1) THEN UseWitness ⌜λx.Ax⌝⋅) }

1
1. T : Type
2. P : T ⟶ ℙ
3. eq : EqDecider(T)
4. s : fset(T)
5. d : ∀x:T. Dec(P[x])
6. ∀x:T. (isl(d x) ∈ 𝔹)
7. ∀x:T. (↑isl(d x) ⇐⇒ P[x])
⊢ λx.Ax ∈ (¬↑fset-null({x ∈ s | isl(d x)})) ⇒ (↓∃x:T. (x ∈ s ∧ P[x]))

---

Latex:

---

Latex:

1.  [T]  :  Type
2.  [P]  :  T  {}\mrightarrow{}  \mBbbP{}
3.  eq  :  EqDecider(T)
4.  s  :  fset(T)
5.  d  :  \mforall{}x:T.  Dec(P[x])
6.  \mforall{}x:T.  (isl(d  x)  \mmember{}  \mBbbB{})
7.  \mforall{}x:T.  (\muparrow{}isl(d  x)  \mLeftarrow{}{}\mRightarrow{}  P[x])
8.  \mneg{}\muparrow{}fset-null(\{x  \mmember{}  s  |  isl(d  x)\})
\mvdash{}  \mdownarrow{}\mexists{}x:T.  (x  \mmember{}  s  \mwedge{}  P[x])


By

---

Latex:
(MoveToConcl  (-1)  THEN  UseWitness  \mkleeneopen{}\mlambda{}x.Ax\mkleeneclose{}\mcdot{})

---

Home Index