---

Step * 1 of Lemma first_index-positive


1. [T] : Type
2. P : T ⟶ 𝔹@i
3. L : T List@i
⊢ ∃i:ℕ||L||. (↑P[L[i]]) ⇐⇒ (∃x∈L. ↑P[x])
BY
{ (Unfold `l_exists` 0 THEN Auto THEN ExRepD) }

---

Latex:

---

Latex:

1.  [T]  :  Type
2.  P  :  T  {}\mrightarrow{}  \mBbbB{}@i
3.  L  :  T  List@i
\mvdash{}  \mexists{}i:\mBbbN{}||L||.  (\muparrow{}P[L[i]])  \mLeftarrow{}{}\mRightarrow{}  (\mexists{}x\mmember{}L.  \muparrow{}P[x])


By

---

Latex:
(Unfold  `l\_exists`  0  THEN  Auto  THEN  ExRepD)

---

Home Index