---

Step * 2 1 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
8. (a ∈ [u / v])
9. ↑P[a]
10. ¬↑P[u]
⊢ (a ∈ v)
BY
{ xxx(((RWO "cons_member" (-3)) THENM (D (-3))) THEN Auto)xxx }

---

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.  a  :  T
8.  (a  \mmember{}  [u  /  v])
9.  \muparrow{}P[a]
10.  \mneg{}\muparrow{}P[u]
\mvdash{}  (a  \mmember{}  v)


By

---

Latex:
xxx(((RWO  "cons\_member"  (-3))  THENM  (D  (-3)))  THEN  Auto)xxx

---

Home Index