---

Step * of Lemma fset-union-associative

∀[A:Type]. ∀[eqa:EqDecider(A)]. ∀[x,y,z:fset(A)].  (x ⋃ y ⋃ z = x ⋃ y ⋃ z ∈ fset(A))
BY
{ ((Auto THEN (Using [`eq',⌜eqa⌝] (BLemma `fset-extensionality` )⋅ THENA Auto))
   THEN Auto
   THEN (RWW "member-fset-union" 0 THENM RWW "member-fset-union" (-1))
   THEN Auto
   THEN ProveProp
   THEN Auto) }

---

Latex:

---

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


By

---

Latex:
((Auto  THEN  (Using  [`eq',\mkleeneopen{}eqa\mkleeneclose{}]  (BLemma  `fset-extensionality`  )\mcdot{}  THENA  Auto))
  THEN  Auto
  THEN  (RWW  "member-fset-union"  0  THENM  RWW  "member-fset-union"  (-1))
  THEN  Auto
  THEN  ProveProp
  THEN  Auto)

---

Home Index