---

Step * of Lemma map-l-union

∀[T,T':Type]. ∀[f:T ⟶ T']. ∀[eq:EqDecider(T)]. ∀[eq':EqDecider(T')]. ∀[as,bs:T List].
  map(f;as ⋃ bs) ~ map(f;as) ⋃ map(f;bs) supposing Inj({x:T| (x ∈ as ⋃ bs)} ;T';f)
BY
{ (Auto
   THEN MoveToConcl (-1)
   THEN MoveToConcl (-2)
   THEN ListInd (-1)
   THEN Reduce 0
   THEN RepUR ``l-union`` 0
   THEN Try (Fold `l-union` 0)
   THEN Auto
   THEN (RWO "-3<" 0 THENA 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. Inj({x:T| (x ∈ insert(u;as ⋃ v))} ;T';f)
⊢ Inj({x:T| (x ∈ as ⋃ v)} ;T';f)

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. Inj({x:T| (x ∈ insert(u;as ⋃ v))} ;T';f)
⊢ map(f;insert(u;as ⋃ v)) ~ insert(f u;map(f;as ⋃ v))

---

Latex:

---

Latex:
\mforall{}[T,T':Type].  \mforall{}[f:T  {}\mrightarrow{}  T'].  \mforall{}[eq:EqDecider(T)].  \mforall{}[eq':EqDecider(T')].  \mforall{}[as,bs:T  List].
    map(f;as  \mcup{}  bs)  \msim{}  map(f;as)  \mcup{}  map(f;bs)  supposing  Inj(\{x:T|  (x  \mmember{}  as  \mcup{}  bs)\}  ;T';f)


By

---

Latex:
(Auto
  THEN  MoveToConcl  (-1)
  THEN  MoveToConcl  (-2)
  THEN  ListInd  (-1)
  THEN  Reduce  0
  THEN  RepUR  ``l-union``  0
  THEN  Try  (Fold  `l-union`  0)
  THEN  Auto
  THEN  (RWO  "-3<"  0  THENA  Auto))

---

Home Index