---

Step * 1 of Lemma find-hd-filter


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

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

---

Latex:

---

Latex:

1.  T  :  Type
2.  P  :  T  {}\mrightarrow{}  \mBbbB{}
3.  d  :  Top
4.  \mexists{}a:T.  ((a  \mmember{}  [])  \mwedge{}  (\muparrow{}P[a]))
\mvdash{}  d  =  hd([])


By

---

Latex:
ExRepD

---

Home Index