---

Step * of Lemma fset-union-commutes

∀[A:Type]. ∀[eqa:EqDecider(A)]. ∀[x,y:fset(A)].  (x ⋃ y = y ⋃ x ∈ fset(A))
BY
{ (Auto THEN (Using [`eq',⌜eqa⌝] (BLemma `fset-extensionality` )⋅ THENA Auto)) }

1
1. A : Type
2. eqa : EqDecider(A)
3. x : fset(A)
4. y : fset(A)
⊢ ∀[a:A]. uiff(a ∈ x ⋃ y;a ∈ y ⋃ x)

---

Latex:

---

Latex:
\mforall{}[A:Type].  \mforall{}[eqa:EqDecider(A)].  \mforall{}[x,y:fset(A)].    (x  \mcup{}  y  =  y  \mcup{}  x)


By

---

Latex:
(Auto  THEN  (Using  [`eq',\mkleeneopen{}eqa\mkleeneclose{}]  (BLemma  `fset-extensionality`  )\mcdot{}  THENA  Auto))

---

Home Index