---

Step * 2 1 of Lemma concat-map-decide


1. T : Type
2. B : T ⟶ (Top + Top)
3. u : T
4. v : T List
5. concat(map(λx.case B[x] of inl(a) => [a] | inr(a) => [];v)) ~ mapfilter(λx.outl(B[x]);λx.isl(B[x]);v)
6. x1 : Top
7. B[u] = (inl x1) ∈ (Top + Top)
8. True
⊢ concat([[x1] / map(λx.case B[x] of inl(a) => [a] | inr(a) => [];v)]) ~ [x1 / mapfilter(λx.outl(B[x]);λx.isl(B[x]);v)]
BY
{ xxx(Unfold `concat` 0 THEN Reduce 0 THEN Fold `concat` 0 THEN EqCD THEN Try (Trivial))xxx }

---

Latex:

---

Latex:

1.  T  :  Type
2.  B  :  T  {}\mrightarrow{}  (Top  +  Top)
3.  u  :  T
4.  v  :  T  List
5.  concat(map(\mlambda{}x.case  B[x]  of  inl(a)  =>  [a]  |  inr(a)  =>  [];v))  \msim{}  mapfilter(\mlambda{}x.outl(B[x]);
                                                                                                                                                      \mlambda{}x.isl(B[x]);
                                                                                                                                                      v)
6.  x1  :  Top
7.  B[u]  =  (inl  x1)
8.  True
\mvdash{}  concat([[x1]  /  map(\mlambda{}x.case  B[x]  of  inl(a)  =>  [a]  |  inr(a)  =>  [];v)])  \msim{}  [x1  / 
                                                                                                                                                    mapfilter(\mlambda{}x.outl(B[x]);
                                                                                                                                                                        \mlambda{}x.isl(B[x]);
                                                                                                                                                                        v)]


By

---

Latex:
xxx(Unfold  `concat`  0  THEN  Reduce  0  THEN  Fold  `concat`  0  THEN  EqCD  THEN  Try  (Trivial))xxx

---

Home Index