---

Step * of Lemma fset-add-remove

∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[s:fset(T)]. ∀[x:T].  fset-add(eq;x;fset-remove(eq;x;s)) = s ∈ fset(T) supposing x ∈ s
BY
{ (Auto THEN FsetExt) }

1
1. T : Type
2. eq : EqDecider(T)
3. s : fset(T)
4. x : T
5. x ∈ s
6. a : T
7. (a = x ∈ T) ∨ (a ∈ s ∧ (¬(a = x ∈ T)))
⊢ a ∈ s

2
1. T : Type
2. eq : EqDecider(T)
3. s : fset(T)
4. x : T
5. x ∈ s
6. a : T
7. a ∈ s
⊢ (a = x ∈ T) ∨ (a ∈ s ∧ (¬(a = x ∈ T)))

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[eq:EqDecider(T)].  \mforall{}[s:fset(T)].  \mforall{}[x:T].
    fset-add(eq;x;fset-remove(eq;x;s))  =  s  supposing  x  \mmember{}  s


By

---

Latex:
(Auto  THEN  FsetExt)

---

Home Index