---

Step * 1 of Lemma assert-bl-exists

.....assertion..... 
∀[T:Type]. ∀P:T ⟶ 𝔹. ∀L:T List.  (↑(∃x∈L.P[x])_b ⇐⇒ (∃x∈L. ↑P[x]))
BY
{ ((UnivCD THENA Auto)
   THEN (RWO "l_exists_iff" 0 THENA Auto)
   THEN ListInd (-1)
   THEN Unfold `bl-exists` 0
   THEN Reduce 0
   THEN Try (Fold `bl-exists` 0)) }

1
1. [T] : Type
2. P : T ⟶ 𝔹@i
⊢ False ⇐⇒ ∃x:T. ((x ∈ []) ∧ (↑P[x]))

2
1. [T] : Type
2. P : T ⟶ 𝔹@i
3. u : T@i
4. v : T List@i
5. ↑(∃x∈v.P[x])_b ⇐⇒ ∃x:T. ((x ∈ v) ∧ (↑P[x]))@i
⊢ ↑(P[u] ∨b(∃x∈v.P[x])_b) ⇐⇒ ∃x:T. ((x ∈ [u / v]) ∧ (↑P[x]))

---

Latex:

---

Latex:
.....assertion..... 
\mforall{}[T:Type].  \mforall{}P:T  {}\mrightarrow{}  \mBbbB{}.  \mforall{}L:T  List.    (\muparrow{}(\mexists{}x\mmember{}L.P[x])\_b  \mLeftarrow{}{}\mRightarrow{}  (\mexists{}x\mmember{}L.  \muparrow{}P[x]))


By

---

Latex:
((UnivCD  THENA  Auto)
  THEN  (RWO  "l\_exists\_iff"  0  THENA  Auto)
  THEN  ListInd  (-1)
  THEN  Unfold  `bl-exists`  0
  THEN  Reduce  0
  THEN  Try  (Fold  `bl-exists`  0))

---

Home Index