---

Step * of Lemma bl-exists-first

∀[A:Type]. ∀P:A ⟶ 𝔹. ∀L:A List.  (↑(∃x∈L.P[x])_b ⇐⇒ ∃i:ℕ||L||. ((↑P[L[i]]) ∧ (∀j:ℕi. (¬↑P[L[j]]))))
BY
{ ((UnivCD THENA Auto) THEN (RWO "assert-bl-exists" 0 THENA Auto) THEN ListInd (-1) THEN Reduce 0) }

1
1. [A] : Type
2. P : A ⟶ 𝔹
⊢ (∃x∈[]. ↑P[x]) ⇐⇒ ∃i:ℕ0. ((↑P[⊥]) ∧ (∀j:ℕi. (¬↑P[⊥])))

2
1. [A] : Type
2. P : A ⟶ 𝔹
3. u : A
4. v : A List
5. (∃x∈v. ↑P[x]) ⇐⇒ ∃i:ℕ||v||. ((↑P[v[i]]) ∧ (∀j:ℕi. (¬↑P[v[j]])))
⊢ (∃x∈[u / v]. ↑P[x]) ⇐⇒ ∃i:ℕ||v|| + 1. ((↑P[[u / v][i]]) ∧ (∀j:ℕi. (¬↑P[[u / v][j]])))

---

Latex:

---

Latex:
\mforall{}[A:Type]
    \mforall{}P:A  {}\mrightarrow{}  \mBbbB{}.  \mforall{}L:A  List.    (\muparrow{}(\mexists{}x\mmember{}L.P[x])\_b  \mLeftarrow{}{}\mRightarrow{}  \mexists{}i:\mBbbN{}||L||.  ((\muparrow{}P[L[i]])  \mwedge{}  (\mforall{}j:\mBbbN{}i.  (\mneg{}\muparrow{}P[L[j]]))))


By

---

Latex:
((UnivCD  THENA  Auto)  THEN  (RWO  "assert-bl-exists"  0  THENA  Auto)  THEN  ListInd  (-1)  THEN  Reduce  0)

---

Home Index