---

Step * 1 1 of Lemma find-hd-filter


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

---

Latex:

---

Latex:

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


By

---

Latex:
ObviousFrom  [(-2)]

---

Home Index