---

Step * of Lemma find-first_wf

∀[T:Type]. ∀[L:T List]. ∀[P:{x:T| (x ∈ L)}  ⟶ 𝔹].  (find-first(P;L) ∈ (∃x:T [first-member(T;x;L;P)]) ∨ (∀x∈L.¬↑(P x)))
BY
{ TACTIC:((BasicUniformUnivCD Auto THEN Unhide) THEN Unfold `find-first` 0) }

1
1. T : Type
2. L : T List
3. P : {x:T| (x ∈ L)}  ⟶ 𝔹
⊢ TERMOF{can-find-first-ext:o, 1:l, 1:l} L P ∈ (∃x:T [first-member(T;x;L;P)]) ∨ (∀x∈L.¬↑(P x))

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[L:T  List].  \mforall{}[P:\{x:T|  (x  \mmember{}  L)\}    {}\mrightarrow{}  \mBbbB{}].
    (find-first(P;L)  \mmember{}  (\mexists{}x:T  [first-member(T;x;L;P)])  \mvee{}  (\mforall{}x\mmember{}L.\mneg{}\muparrow{}(P  x)))


By

---

Latex:
TACTIC:((BasicUniformUnivCD  Auto  THEN  Unhide)  THEN  Unfold  `find-first`  0)

---

Home Index