---

Step * 1 2 of Lemma can-find-first2

.....eq aux..... 
1. T : Type
2. L : T List
3. P : {x:T| (x ∈ L)}  ⟶ 𝔹
4. y : (∀x∈L.¬↑(P x))
⊢ ∃x:T [first-member(T;x;L;P)] ∈ Type
BY
{ (Unfold `first-member` 0 THEN Auto) }

---

Latex:

---

Latex:
.....eq  aux..... 
1.  T  :  Type
2.  L  :  T  List
3.  P  :  \{x:T|  (x  \mmember{}  L)\}    {}\mrightarrow{}  \mBbbB{}
4.  y  :  (\mforall{}x\mmember{}L.\mneg{}\muparrow{}(P  x))
\mvdash{}  \mexists{}x:T  [first-member(T;x;L;P)]  \mmember{}  Type


By

---

Latex:
(Unfold  `first-member`  0  THEN  Auto)

---

Home Index