---

Step * of Lemma find-hd-filter

∀[T:Type]. ∀[P:T ⟶ 𝔹]. ∀[as:T List]. ∀[d:Top].
  (first a ∈ as s.t. P[a] else d) = hd(filter(λa.P[a];as)) ∈ T supposing ∃a:T. ((a ∈ as) ∧ (↑P[a]))
BY
{ xxx(InductionOnList THEN Unfold `find` 0 THEN Reduce 0 THEN Auto)xxx }

1
1. T : Type
2. P : T ⟶ 𝔹
3. d : Top
4. ∃a:T. ((a ∈ []) ∧ (↑P[a]))
⊢ d = hd([]) ∈ T

2
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]))
⊢ case if P[u] then [u / filter(λa.P[a];v)] else filter(λa.P[a];v) fi  of [] => d | a::b => a esac
= hd(if P[u] then [u / filter(λa.P[a];v)] else filter(λa.P[a];v) fi )
∈ T

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[P:T  {}\mrightarrow{}  \mBbbB{}].  \mforall{}[as:T  List].  \mforall{}[d:Top].
    (first  a  \mmember{}  as  s.t.  P[a]  else  d)  =  hd(filter(\mlambda{}a.P[a];as))  supposing  \mexists{}a:T.  ((a  \mmember{}  as)  \mwedge{}  (\muparrow{}P[a]))


By

---

Latex:
xxx(InductionOnList  THEN  Unfold  `find`  0  THEN  Reduce  0  THEN  Auto)xxx

---

Home Index