---

Step * of Lemma member-fset-list-union

∀[T:Type]. ∀eq:EqDecider(T). ∀ss:fset(T) List. ∀x:T.  (x ∈ fset-list-union(eq;ss) ⇐⇒ (∃s∈ss. x ∈ s))
BY
{ (InductionOnList
   THEN Unfold `fset-list-union` 0
   THEN Reduce 0
   THEN Try (Fold `fset-list-union` 0)
   THEN RWW "l_exists_nil l_exists_cons member-fset-union" 0⋅
   THEN Auto
   THEN SplitOrHyps
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[T:Type]
    \mforall{}eq:EqDecider(T).  \mforall{}ss:fset(T)  List.  \mforall{}x:T.    (x  \mmember{}  fset-list-union(eq;ss)  \mLeftarrow{}{}\mRightarrow{}  (\mexists{}s\mmember{}ss.  x  \mmember{}  s))


By

---

Latex:
(InductionOnList
  THEN  Unfold  `fset-list-union`  0
  THEN  Reduce  0
  THEN  Try  (Fold  `fset-list-union`  0)
  THEN  RWW  "l\_exists\_nil  l\_exists\_cons  member-fset-union"  0\mcdot{}
  THEN  Auto
  THEN  SplitOrHyps
  THEN  Auto)

---

Home Index