---

Step * of Lemma empty-fset-union

∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[s:fset(T)].  ({} ⋃ s = s ∈ fset(T))
BY
{ (Auto THEN (UsingVars [`eq'] (BLemma `fset-extensionality`) THENA Auto)) }

1
1. T : Type
2. eq : EqDecider(T)
3. s : fset(T)
⊢ ∀[a:T]. uiff(a ∈ {} ⋃ s;a ∈ s)

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[eq:EqDecider(T)].  \mforall{}[s:fset(T)].    (\{\}  \mcup{}  s  =  s)


By

---

Latex:
(Auto  THEN  (UsingVars  [`eq']  (BLemma  `fset-extensionality`)  THENA  Auto))

---

Home Index