---

Step * 1 of Lemma map-l-union


1. T : Type
2. T' : Type
3. f : T ⟶ T'
4. eq : EqDecider(T)
5. eq' : EqDecider(T')
6. u : T
7. v : T List
8. ∀as:T List. (Inj({x:T| (x ∈ as ⋃ v)} ;T';f) ⇒ (map(f;as ⋃ v) ~ map(f;as) ⋃ map(f;v)))
9. as : T List
10. Inj({x:T| (x ∈ insert(u;as ⋃ v))} ;T';f)
⊢ Inj({x:T| (x ∈ as ⋃ v)} ;T';f)
BY
{ (RepeatFor 3 ((ParallelLast THENA ((D -1 THEN MemTypeCD THEN Auto) THEN RWO "member-insert" 0 THEN Auto)))
   THEN Auto
   ) }

---

Latex:

---

Latex:

1.  T  :  Type
2.  T'  :  Type
3.  f  :  T  {}\mrightarrow{}  T'
4.  eq  :  EqDecider(T)
5.  eq'  :  EqDecider(T')
6.  u  :  T
7.  v  :  T  List
8.  \mforall{}as:T  List.  (Inj(\{x:T|  (x  \mmember{}  as  \mcup{}  v)\}  ;T';f)  {}\mRightarrow{}  (map(f;as  \mcup{}  v)  \msim{}  map(f;as)  \mcup{}  map(f;v)))
9.  as  :  T  List
10.  Inj(\{x:T|  (x  \mmember{}  insert(u;as  \mcup{}  v))\}  ;T';f)
\mvdash{}  Inj(\{x:T|  (x  \mmember{}  as  \mcup{}  v)\}  ;T';f)


By

---

Latex:
(RepeatFor  3  ((ParallelLast
                              THENA  ((D  -1  THEN  MemTypeCD  THEN  Auto)  THEN  RWO  "member-insert"  0  THEN  Auto)
                              ))
  THEN  Auto
  )

---

Home Index