---

Step * of Lemma bag-member-decidable2

∀T:Type. ∀P:T ⟶ ℙ. ∀b:bag(T). ∀x:{x:T| P[x]} .
  ((∀x,y:{x:T| P[x]} .  Dec(x = y ∈ {x:T| P[x]} )) ⇒ (∀x:{x:T| x ↓∈ b} . ∃y:{x:T| P[x]} . (x = y ∈ T)) ⇒ Dec(x ↓∈ b))
BY
{ TACTIC:(UnivCD THENA Auto) }

1
1. T : Type
2. P : T ⟶ ℙ
3. b : bag(T)
4. x : {x:T| P[x]} 
5. ∀x,y:{x:T| P[x]} .  Dec(x = y ∈ {x:T| P[x]} )
6. ∀x:{x:T| x ↓∈ b} . ∃y:{x:T| P[x]} . (x = y ∈ T)
⊢ Dec(x ↓∈ b)

---

Latex:

---

Latex:
\mforall{}T:Type.  \mforall{}P:T  {}\mrightarrow{}  \mBbbP{}.  \mforall{}b:bag(T).  \mforall{}x:\{x:T|  P[x]\}  .
    ((\mforall{}x,y:\{x:T|  P[x]\}  .    Dec(x  =  y))  {}\mRightarrow{}  (\mforall{}x:\{x:T|  x  \mdownarrow{}\mmember{}  b\}  .  \mexists{}y:\{x:T|  P[x]\}  .  (x  =  y))  {}\mRightarrow{}  Dec(x  \mdownarrow{}\mmember{}  b))


By

---

Latex:
TACTIC:(UnivCD  THENA  Auto)

---

Home Index