---

Step * of Lemma member-fset-union

∀[T:Type]. ∀eq:EqDecider(T). ∀x,y:fset(T). ∀a:T.  (a ∈ x ⋃ y ⇐⇒ a ∈ x ∨ a ∈ y)
BY
{ (Auto
   THEN (SupposeNot THENM Assert ⌜0 = 1 ∈ ℤ⌝⋅)
   THEN Auto
   THEN (Dquotient2 4 THENA Auto)
   THEN (Dquotient2 3 THENA Auto)
   THEN D -1
   THEN All (\h. (Unfolds ``fset-member fset-union`` h THEN (RW assert_pushdownC h THENA Auto)))⋅
   THEN Using [`eq',⌜eq⌝] (BLemma `member-union`)⋅
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}eq:EqDecider(T).  \mforall{}x,y:fset(T).  \mforall{}a:T.    (a  \mmember{}  x  \mcup{}  y  \mLeftarrow{}{}\mRightarrow{}  a  \mmember{}  x  \mvee{}  a  \mmember{}  y)


By

---

Latex:
(Auto
  THEN  (SupposeNot  THENM  Assert  \mkleeneopen{}0  =  1\mkleeneclose{}\mcdot{})
  THEN  Auto
  THEN  (Dquotient2  4  THENA  Auto)
  THEN  (Dquotient2  3  THENA  Auto)
  THEN  D  -1
  THEN  All  (\mbackslash{}h.  (Unfolds  ``fset-member  fset-union``  h  THEN  (RW  assert\_pushdownC  h  THENA  Auto)))\mcdot{}
  THEN  Using  [`eq',\mkleeneopen{}eq\mkleeneclose{}]  (BLemma  `member-union`)\mcdot{}
  THEN  Auto)

---

Home Index