---

Step * of Lemma f-union_wf

∀[T,A:Type]. ∀[eqt:EqDecider(T)]. ∀[eqa:EqDecider(A)]. ∀[g:T ⟶ fset(A)]. ∀[s:fset(T)].
  (f-union(eqt;eqa;s;x.g[x]) ∈ fset(A))
BY
{ (((Auto THEN D -1) THENA Auto) THEN Unfold `f-union` 0) }

1
1. T : Type
2. A : Type
3. eqt : EqDecider(T)
4. eqa : EqDecider(A)
5. g : T ⟶ fset(A)
6. s : Base
7. s1 : Base
8. s = s1 ∈ pertype(λx,y. ((x ∈ T List) ∧ (y ∈ T List) ∧ set-equal(T;x;y)))
9. s ∈ T List
10. s1 ∈ T List
11. set-equal(T;s;s1)
⊢ accumulate (with value a and list item x):
   a ⋃ g[x]
  over list:
    s
  with starting value:
   [])
= accumulate (with value a and list item x):
   a ⋃ g[x]
  over list:
    s1
  with starting value:
   [])
∈ fset(A)

---

Latex:

---

Latex:
\mforall{}[T,A:Type].  \mforall{}[eqt:EqDecider(T)].  \mforall{}[eqa:EqDecider(A)].  \mforall{}[g:T  {}\mrightarrow{}  fset(A)].  \mforall{}[s:fset(T)].
    (f-union(eqt;eqa;s;x.g[x])  \mmember{}  fset(A))


By

---

Latex:
(((Auto  THEN  D  -1)  THENA  Auto)  THEN  Unfold  `f-union`  0)

---

Home Index