---

Step * of Lemma fset-size-remove

∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[s:fset(T)]. ∀[x:T].  ||fset-remove(eq;x;s)|| = (||s|| - 1) ∈ ℤ supposing x ∈ s
BY
{ (Auto THEN newQuotD 3 THEN Auto) }

1
1. T : Type
2. eq : EqDecider(T)
3. istype(T List)
4. ∀x1,y:T List.  istype(set-equal(T;x1;y))
5. ∀x1:T List. set-equal(T;x1;x1)
6. a : Base
7. b : Base
8. c : a = b ∈ pertype(λx,y. ((x ∈ T List) ∧ (y ∈ T List) ∧ set-equal(T;x;y)))
9. a ∈ T List
10. b ∈ T List
11. set-equal(T;a;b)
12. x : T
13. x ∈ a
⊢ ||fset-remove(eq;x;a)|| = (||a|| - 1) ∈ ℤ

---

Latex:

---

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


By

---

Latex:
(Auto  THEN  newQuotD  3  THEN  Auto)

---

Home Index