---

Step * 2 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. ¬(f u ∈ map(f;as ⋃ v))
11. Inj({x:T| (x ∈ insert(u;as ⋃ v))} ;T';f)
12. (u ∈ as ⋃ v)
⊢ map(f;as ⋃ v) ~ [f u / map(f;as ⋃ v)]
BY
{ (D -3 THEN BLemma `member-map` 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.  \mneg{}(f  u  \mmember{}  map(f;as  \mcup{}  v))
11.  Inj(\{x:T|  (x  \mmember{}  insert(u;as  \mcup{}  v))\}  ;T';f)
12.  (u  \mmember{}  as  \mcup{}  v)
\mvdash{}  map(f;as  \mcup{}  v)  \msim{}  [f  u  /  map(f;as  \mcup{}  v)]


By

---

Latex:
(D  -3  THEN  BLemma  `member-map`  THEN  Auto)

---

Home Index