---

Step * 2 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. ¬(u ∈ as ⋃ v)
11. Inj({x:T| (x ∈ insert(u;as ⋃ v))} ;T';f)
12. y : T
13. (y ∈ as ⋃ v)
14. (f u) = (f y) ∈ T'
⊢ [f u / map(f;as ⋃ v)] ~ map(f;as ⋃ v)
BY
{ ((With ⌜u⌝ (D (-4))⋅ THENA (MemTypeCD THEN Auto THEN BLemma `member-insert` THEN Auto))
   THEN (FHyp (-1) [-2] THENA (MemTypeCD THEN Auto THEN BLemma `member-insert` THEN Auto))
   ) }

1
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. ¬(u ∈ as ⋃ v)
11. y : T
12. (y ∈ as ⋃ v)
13. (f u) = (f y) ∈ T'
14. ∀a2:{x:T| (x ∈ insert(u;as ⋃ v))} . (((f u) = (f a2) ∈ T') ⇒ (u = a2 ∈ {x:T| (x ∈ insert(u;as ⋃ v))} ))
15. u = y ∈ {x:T| (x ∈ insert(u;as ⋃ v))} 
⊢ [f u / map(f;as ⋃ v)] ~ map(f;as ⋃ v)

---

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{}(u  \mmember{}  as  \mcup{}  v)
11.  Inj(\{x:T|  (x  \mmember{}  insert(u;as  \mcup{}  v))\}  ;T';f)
12.  y  :  T
13.  (y  \mmember{}  as  \mcup{}  v)
14.  (f  u)  =  (f  y)
\mvdash{}  [f  u  /  map(f;as  \mcup{}  v)]  \msim{}  map(f;as  \mcup{}  v)


By

---

Latex:
((With  \mkleeneopen{}u\mkleeneclose{}  (D  (-4))\mcdot{}  THENA  (MemTypeCD  THEN  Auto  THEN  BLemma  `member-insert`  THEN  Auto))
  THEN  (FHyp  (-1)  [-2]  THENA  (MemTypeCD  THEN  Auto  THEN  BLemma  `member-insert`  THEN  Auto))
  )

---

Home Index