---

Step * 1 2 1 of Lemma finite-set-type-cases


1. [T] : Type
2. L : (T ⟶ ℙ) List
3. [P] : T ⟶ ℙ
4. ∀x:T. Dec(P[x])
5. (∀Q∈L.∀x:T. Dec(Q[x]))
6. (∀Q∈L.finite-type({x:T| Q[x]} ))
7. ∀x:T. (P[x] ⇒ (∃Q∈L. Q[x]))
8. f : ∀i:ℕ||L||. ∃L1:T List. ∀x:T. (L[i][x] ⇒ (x ∈ L1))
9. x : T
10. P[x]
⊢ (x ∈ concat(map(λi.(fst((f i)));upto(||L||))))
BY
{ xxx(RWO "member-concat" 0 THEN Auto' THEN RWO "member_map" 0 THEN Reduce 0 THEN Auto')xxx }

1
1. [T] : Type
2. L : (T ⟶ ℙ) List
3. [P] : T ⟶ ℙ
4. ∀x:T. Dec(P[x])
5. (∀Q∈L.∀x:T. Dec(Q[x]))
6. (∀Q∈L.finite-type({x:T| Q[x]} ))
7. ∀x:T. (P[x] ⇒ (∃Q∈L. Q[x]))
8. f : ∀i:ℕ||L||. ∃L1:T List. ∀x:T. (L[i][x] ⇒ (x ∈ L1))
9. x : T
10. P[x]
⊢ ∃l:T List. ((∃y:ℕ||L||. ((y ∈ upto(||L||)) ∧ (l = (fst((f y))) ∈ (T List)))) ∧ (x ∈ l))

---

Latex:

---

Latex:

1.  [T]  :  Type
2.  L  :  (T  {}\mrightarrow{}  \mBbbP{})  List
3.  [P]  :  T  {}\mrightarrow{}  \mBbbP{}
4.  \mforall{}x:T.  Dec(P[x])
5.  (\mforall{}Q\mmember{}L.\mforall{}x:T.  Dec(Q[x]))
6.  (\mforall{}Q\mmember{}L.finite-type(\{x:T|  Q[x]\}  ))
7.  \mforall{}x:T.  (P[x]  {}\mRightarrow{}  (\mexists{}Q\mmember{}L.  Q[x]))
8.  f  :  \mforall{}i:\mBbbN{}||L||.  \mexists{}L1:T  List.  \mforall{}x:T.  (L[i][x]  {}\mRightarrow{}  (x  \mmember{}  L1))
9.  x  :  T
10.  P[x]
\mvdash{}  (x  \mmember{}  concat(map(\mlambda{}i.(fst((f  i)));upto(||L||))))


By

---

Latex:
xxx(RWO  "member-concat"  0  THEN  Auto'  THEN  RWO  "member\_map"  0  THEN  Reduce  0  THEN  Auto')xxx

---

Home Index