---

Step * 1 of Lemma finite-subtype


1. [B] : Type
2. P : B ⟶ 𝔹@i
3. L : B List@i
4. ∀x:B. (x ∈ L)@i
⊢ ∃L:{b:B| ↑P[b]}  List. ∀x:{b:B| ↑P[b]} . (x ∈ L)
BY
{ (((InstLemma `filter_type` [⌜B⌝; ⌜P⌝; ⌜L⌝])⋅ THENA Auto)
   THEN (InstConcl [⌜filter(P;L)⌝])⋅
   THEN Auto
   THEN Assert ⌜(x ∈ filter(P;L))⌝⋅) }

---

Latex:

---

Latex:

1.  [B]  :  Type
2.  P  :  B  {}\mrightarrow{}  \mBbbB{}@i
3.  L  :  B  List@i
4.  \mforall{}x:B.  (x  \mmember{}  L)@i
\mvdash{}  \mexists{}L:\{b:B|  \muparrow{}P[b]\}    List.  \mforall{}x:\{b:B|  \muparrow{}P[b]\}  .  (x  \mmember{}  L)


By

---

Latex:
(((InstLemma  `filter\_type`  [\mkleeneopen{}B\mkleeneclose{};  \mkleeneopen{}P\mkleeneclose{};  \mkleeneopen{}L\mkleeneclose{}])\mcdot{}  THENA  Auto)
  THEN  (InstConcl  [\mkleeneopen{}filter(P;L)\mkleeneclose{}])\mcdot{}
  THEN  Auto
  THEN  Assert  \mkleeneopen{}(x  \mmember{}  filter(P;L))\mkleeneclose{}\mcdot{})

---

Home Index