---

Step * of Lemma concat-map-decide

∀[T:Type]. ∀[B:T ⟶ (Top + Top)]. ∀[L:T List].
  (concat(map(λx.case B[x] of inl(a) => [a] | inr(a) => [];L)) ~ mapfilter(λx.outl(B[x]);λx.isl(B[x]);L))
BY
{ xxx(InductionOnList THEN Reduce 0)xxx }

1
1. T : Type
2. B : T ⟶ (Top + Top)
⊢ [] ~ []

2
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)
⊢ concat([case B[u] of inl(a) => [a] | inr(a) => [] / map(λx.case B[x] of inl(a) => [a] | inr(a) => [];v)]) 
~ mapfilter(λx.outl(B[x]);λx.isl(B[x]);[u / v])

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[B:T  {}\mrightarrow{}  (Top  +  Top)].  \mforall{}[L:T  List].
    (concat(map(\mlambda{}x.case  B[x]  of  inl(a)  =>  [a]  |  inr(a)  =>  [];L))  \msim{}  mapfilter(\mlambda{}x.outl(B[x]);
                                                                                                                                                      \mlambda{}x.isl(B[x]);
                                                                                                                                                      L))


By

---

Latex:
xxx(InductionOnList  THEN  Reduce  0)xxx

---

Home Index