---

Step * 1 of Lemma fset-size-union


1. T : Type
2. valueall-type(T)
3. eq : EqDecider(T)
4. b : fset(T)
⊢ ||{} ⋃ b|| = ((||{}|| + ||b||) - ||{} ⋂ b||) ∈ ℤ
BY
{ (Subst' {} ⋃ b = b ∈ fset(T) 0 THEN Auto THEN Reduce 0 THEN Auto) }

---

Latex:

---

Latex:

1.  T  :  Type
2.  valueall-type(T)
3.  eq  :  EqDecider(T)
4.  b  :  fset(T)
\mvdash{}  ||\{\}  \mcup{}  b||  =  ((||\{\}||  +  ||b||)  -  ||\{\}  \mcap{}  b||)


By

---

Latex:
(Subst'  \{\}  \mcup{}  b  =  b  0  THEN  Auto  THEN  Reduce  0  THEN  Auto)

---

Home Index