---

Step * 1 of Lemma fset-union-commutes


1. A : Type
2. eqa : EqDecider(A)
3. x : fset(A)
4. y : fset(A)
⊢ ∀[a:A]. uiff(a ∈ x ⋃ y;a ∈ y ⋃ x)
BY
{ (Auto THEN (RWO "member-fset-union" 0 THEN Auto)⋅ THEN ((RWO "member-fset-union" (-1) THENM D -1) THEN Auto)⋅) }

---

Latex:

---

Latex:

1.  A  :  Type
2.  eqa  :  EqDecider(A)
3.  x  :  fset(A)
4.  y  :  fset(A)
\mvdash{}  \mforall{}[a:A].  uiff(a  \mmember{}  x  \mcup{}  y;a  \mmember{}  y  \mcup{}  x)


By

---

Latex:
(Auto
  THEN  (RWO  "member-fset-union"  0  THEN  Auto)\mcdot{}
  THEN  ((RWO  "member-fset-union"  (-1)  THENM  D  -1)  THEN  Auto)\mcdot{})

---

Home Index