---

Step * 2 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)
⊢ map(f;insert(u;as ⋃ v)) ~ insert(f u;map(f;as ⋃ v))
BY
{ (Unfold `insert` 0
   THEN (RWO "eval_list_sq" 0 THENA Auto)
   THEN (CallByValueReduce 0 THENA Auto)
   THEN RepeatFor 2 (AutoSplit)) }

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. ¬(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)]

2
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. (f u ∈ map(f;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.  Inj(\{x:T|  (x  \mmember{}  insert(u;as  \mcup{}  v))\}  ;T';f)
\mvdash{}  map(f;insert(u;as  \mcup{}  v))  \msim{}  insert(f  u;map(f;as  \mcup{}  v))


By

---

Latex:
(Unfold  `insert`  0
  THEN  (RWO  "eval\_list\_sq"  0  THENA  Auto)
  THEN  (CallByValueReduce  0  THENA  Auto)
  THEN  RepeatFor  2  (AutoSplit))

---

Home Index