---

Step * 2 1 of Lemma find-hd-filter


1. T : Type
2. P : T ⟶ 𝔹
3. u : T
4. v : T List
5. ∀[d:Top]. (first a ∈ v s.t. P[a] else d) = hd(filter(λa.P[a];v)) ∈ T supposing ∃a:T. ((a ∈ v) ∧ (↑P[a]))
6. d : Top
7. ∃a:T. ((a ∈ [u / v]) ∧ (↑P[a]))
8. ¬↑P[u]
⊢ ∃a:T. ((a ∈ v) ∧ (↑P[a]))
BY
{ xxx((ParallelOp (-2)) THEN Auto)xxx }

1
1. T : Type
2. P : T ⟶ 𝔹
3. u : T
4. v : T List
5. ∀[d:Top]. (first a ∈ v s.t. P[a] else d) = hd(filter(λa.P[a];v)) ∈ T supposing ∃a:T. ((a ∈ v) ∧ (↑P[a]))
6. d : Top
7. a : T
8. (a ∈ [u / v])
9. ↑P[a]
10. ¬↑P[u]
⊢ (a ∈ v)

---

Latex:

---

Latex:

1.  T  :  Type
2.  P  :  T  {}\mrightarrow{}  \mBbbB{}
3.  u  :  T
4.  v  :  T  List
5.  \mforall{}[d:Top]
          (first  a  \mmember{}  v  s.t.  P[a]  else  d)  =  hd(filter(\mlambda{}a.P[a];v))  supposing  \mexists{}a:T.  ((a  \mmember{}  v)  \mwedge{}  (\muparrow{}P[a]))
6.  d  :  Top
7.  \mexists{}a:T.  ((a  \mmember{}  [u  /  v])  \mwedge{}  (\muparrow{}P[a]))
8.  \mneg{}\muparrow{}P[u]
\mvdash{}  \mexists{}a:T.  ((a  \mmember{}  v)  \mwedge{}  (\muparrow{}P[a]))


By

---

Latex:
xxx((ParallelOp  (-2))  THEN  Auto)xxx

---

Home Index