---

Step * of Lemma fset-subtype2

∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[s:fset(T)].  (s ∈ fset({z:T| z ∈ s} ))
BY
{ (Auto THEN D -1 THEN RepUR ``fset fset-member`` 0 THEN EqTypeCD THEN Auto) }

1
.....wf..... 
1. T : Type
2. eq : EqDecider(T)
3. s : Base
4. s1 : Base
5. s = s1 ∈ (x,y:T List//set-equal(T;x;y))
6. s ∈ T List
7. s1 ∈ T List
8. set-equal(T;s;s1)
⊢ s1 ∈ {z:T| ↑z ∈b s}  List

2
.....antecedent..... 
1. T : Type
2. eq : EqDecider(T)
3. s : Base
4. s1 : Base
5. s = s1 ∈ (x,y:T List//set-equal(T;x;y))
6. s ∈ T List
7. s1 ∈ T List
8. set-equal(T;s;s1)
⊢ set-equal({z:T| ↑z ∈b s} ;s;s1)

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[eq:EqDecider(T)].  \mforall{}[s:fset(T)].    (s  \mmember{}  fset(\{z:T|  z  \mmember{}  s\}  ))


By

---

Latex:
(Auto  THEN  D  -1  THEN  RepUR  ``fset  fset-member``  0  THEN  EqTypeCD  THEN  Auto)

---

Home Index