---

Step * of Lemma map_functionality

∀[T,A:Type]. ∀[L1,L2:T List]. ∀[f,g:{x:T| (x ∈ L1)}  ⟶ A].
  (map(f;L1) = map(g;L2) ∈ (A List)) supposing ((f = g ∈ ({x:T| (x ∈ L1)}  ⟶ A)) and (L1 = L2 ∈ (T List)))
BY
{ (Auto
   THEN (GenConcl ⌜L1 = as ∈ ({x:T| (x ∈ L1)}  List)⌝⋅ THENA Auto)
   THEN (GenConcl ⌜L2 = bs ∈ ({x:T| (x ∈ L1)}  List)⌝⋅ THENA Auto)) }

1
.....wf..... 
1. T : Type
2. A : Type
3. L1 : T List
4. L2 : T List
5. f : {x:T| (x ∈ L1)}  ⟶ A
6. g : {x:T| (x ∈ L1)}  ⟶ A
7. L1 = L2 ∈ (T List)
8. f = g ∈ ({x:T| (x ∈ L1)}  ⟶ A)
9. as : {x:T| (x ∈ L1)}  List
10. L1 = as ∈ ({x:T| (x ∈ L1)}  List)
⊢ L2 ∈ {x:T| (x ∈ L1)}  List

2
1. T : Type
2. A : Type
3. L1 : T List
4. L2 : T List
5. f : {x:T| (x ∈ L1)}  ⟶ A
6. g : {x:T| (x ∈ L1)}  ⟶ A
7. L1 = L2 ∈ (T List)
8. f = g ∈ ({x:T| (x ∈ L1)}  ⟶ A)
9. as : {x:T| (x ∈ L1)}  List
10. L1 = as ∈ ({x:T| (x ∈ L1)}  List)
11. bs : {x:T| (x ∈ L1)}  List
12. L2 = bs ∈ ({x:T| (x ∈ L1)}  List)
⊢ map(f;as) = map(g;bs) ∈ (A List)

---

Latex:

---

Latex:
\mforall{}[T,A:Type].  \mforall{}[L1,L2:T  List].  \mforall{}[f,g:\{x:T|  (x  \mmember{}  L1)\}    {}\mrightarrow{}  A].
    (map(f;L1)  =  map(g;L2))  supposing  ((f  =  g)  and  (L1  =  L2))


By

---

Latex:
(Auto  THEN  (GenConcl  \mkleeneopen{}L1  =  as\mkleeneclose{}\mcdot{}  THENA  Auto)  THEN  (GenConcl  \mkleeneopen{}L2  =  bs\mkleeneclose{}\mcdot{}  THENA  Auto))

---

Home Index