---

Step * 1 1 2 of Lemma hd-filter


1. [T] : Type
2. P : T ⟶ 𝔹
3. as : T List
4. ∃a:T. ((a ∈ as) ∧ (↑P[a]))
5. filter(λa.P[a];as) ∈ {x:T| ↑((λa.P[a]) x)}  List
6. v : {x:T| ↑((λa.P[a]) x)}  List
7. filter(λa.P[a];as) = v ∈ ({x:T| ↑((λa.P[a]) x)}  List)
8. 0 < ||v||
9. hd(v) ∈ T
10. (hd(v) ∈ v)
⊢ (hd(v) ∈ as)
BY
{ xxx(MoveToConcl (-1) THEN GenConclTerm ⌜hd(v)⌝⋅ THEN Auto)xxx }

1
1. [T] : Type
2. P : T ⟶ 𝔹
3. as : T List
4. ∃a:T. ((a ∈ as) ∧ (↑P[a]))
5. filter(λa.P[a];as) ∈ {x:T| ↑((λa.P[a]) x)}  List
6. v : {x:T| ↑((λa.P[a]) x)}  List
7. filter(λa.P[a];as) = v ∈ ({x:T| ↑((λa.P[a]) x)}  List)
8. 0 < ||v||
9. hd(v) ∈ T
10. v1 : T
11. hd(v) = v1 ∈ T
12. (v1 ∈ v)
⊢ (v1 ∈ as)

---

Latex:

---

Latex:

1.  [T]  :  Type
2.  P  :  T  {}\mrightarrow{}  \mBbbB{}
3.  as  :  T  List
4.  \mexists{}a:T.  ((a  \mmember{}  as)  \mwedge{}  (\muparrow{}P[a]))
5.  filter(\mlambda{}a.P[a];as)  \mmember{}  \{x:T|  \muparrow{}((\mlambda{}a.P[a])  x)\}    List
6.  v  :  \{x:T|  \muparrow{}((\mlambda{}a.P[a])  x)\}    List
7.  filter(\mlambda{}a.P[a];as)  =  v
8.  0  <  ||v||
9.  hd(v)  \mmember{}  T
10.  (hd(v)  \mmember{}  v)
\mvdash{}  (hd(v)  \mmember{}  as)


By

---

Latex:
xxx(MoveToConcl  (-1)  THEN  GenConclTerm  \mkleeneopen{}hd(v)\mkleeneclose{}\mcdot{}  THEN  Auto)xxx

---

Home Index