---

Step * 2 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]))
⊢ 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
BY
{ xxx(SplitOnConclITE THEN Reduce 0 THEN Auto THEN Fold `find` 0 THEN BackThruSomeHyp 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. ((a ∈ [u / v]) ∧ (↑P[a]))
8. ¬↑P[u]
⊢ ∃a:T. ((a ∈ v) ∧ (↑P[a]))

---

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]))
\mvdash{}  case  if  P[u]  then  [u  /  filter(\mlambda{}a.P[a];v)]  else  filter(\mlambda{}a.P[a];v)  fi    of  []  =>  d  |  a::b  =>  a  esac
=  hd(if  P[u]  then  [u  /  filter(\mlambda{}a.P[a];v)]  else  filter(\mlambda{}a.P[a];v)  fi  )


By

---

Latex:
xxx(SplitOnConclITE  THEN  Reduce  0  THEN  Auto  THEN  Fold  `find`  0  THEN  BackThruSomeHyp  THEN  Auto)xxx

---

Home Index