---

Step * 1 1 of Lemma map-concat-filter-lemma1


1. A : Type
2. B : Type
3. L2 : (tg:Id × (A ─→ B ─→ (Top List))) List
4. L : (Top × Id × Top) List
5. tg : Id
6. a : A
7. b : B
8. map(λx.(snd(x));L) = concat(map(λtgf.map(λx.<fst(tgf), x>;(snd(tgf)) a b);L2)) ∈ ((tg:Id × Top) List)
9. x : Top × Id × Top
10. (x ∈ L)
11. ↑fst(snd(x)) = tg
⊢ (tg ∈ map(λp.(fst(p));L2))
BY
{ ((RWO "assert-eq-id" (-1)) THEN Auto) }

1
1. A : Type
2. B : Type
3. L2 : (tg:Id × (A ─→ B ─→ (Top List))) List
4. L : (Top × Id × Top) List
5. tg : Id
6. a : A
7. b : B
8. map(λx.(snd(x));L) = concat(map(λtgf.map(λx.<fst(tgf), x>;(snd(tgf)) a b);L2)) ∈ ((tg:Id × Top) List)
9. x : Top × Id × Top
10. (x ∈ L)
11. (fst(snd(x))) = tg ∈ Id
⊢ (tg ∈ map(λp.(fst(p));L2))

---

Latex:



1.  A  :  Type
2.  B  :  Type
3.  L2  :  (tg:Id  \mtimes{}  (A  {}\mrightarrow{}  B  {}\mrightarrow{}  (Top  List)))  List
4.  L  :  (Top  \mtimes{}  Id  \mtimes{}  Top)  List
5.  tg  :  Id
6.  a  :  A
7.  b  :  B
8.  map(\mlambda{}x.(snd(x));L)  =  concat(map(\mlambda{}tgf.map(\mlambda{}x.<fst(tgf),  x>(snd(tgf))  a  b);L2))
9.  x  :  Top  \mtimes{}  Id  \mtimes{}  Top
10.  (x  \mmember{}  L)
11.  \muparrow{}fst(snd(x))  =  tg
\mvdash{}  (tg  \mmember{}  map(\mlambda{}p.(fst(p));L2))


By

((RWO  "assert-eq-id"  (-1))  THEN  Auto)

---

Home Index