---

Step * 2 2 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. y : Top
7. B[u] = (inr y ) ∈ (Top + Top)
8. ¬False
⊢ concat([[] / map(λx.case B[x] of inl(a) => [a] | inr(a) => [];v)]) ~ mapfilter(λx.outl(B[x]);λx.isl(B[x]);v)
BY
{ xxx(Unfold `concat` 0 THEN Reduce 0 THEN Fold `concat` 0 THEN Auto)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.  y  :  Top
7.  B[u]  =  (inr  y  )
8.  \mneg{}False
\mvdash{}  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)


By

---

Latex:
xxx(Unfold  `concat`  0  THEN  Reduce  0  THEN  Fold  `concat`  0  THEN  Auto)xxx

---

Home Index