---

Step * 1 2 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. ∀i:ℕ||L||. ∃L1:T List. ∀x:T. (L[i][x] ⇒ (x ∈ L1))
⊢ ∃L:T List. ∀x:T. (P[x] ⇒ (x ∈ L))
BY
{ xxx((RenameVar `f' (-1)) THEN (InstConcl [⌜concat(map(λi.(fst((f i)));upto(||L||)))⌝])⋅ 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]
⊢ (x ∈ concat(map(λi.(fst((f i)));upto(||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.  \mforall{}i:\mBbbN{}||L||.  \mexists{}L1:T  List.  \mforall{}x:T.  (L[i][x]  {}\mRightarrow{}  (x  \mmember{}  L1))
\mvdash{}  \mexists{}L:T  List.  \mforall{}x:T.  (P[x]  {}\mRightarrow{}  (x  \mmember{}  L))


By

---

Latex:
xxx((RenameVar  `f'  (-1))
        THEN  (InstConcl  [\mkleeneopen{}concat(map(\mlambda{}i.(fst((f  i)));upto(||L||)))\mkleeneclose{}])\mcdot{}
        THEN  Auto')xxx

---

Home Index