---

Step * of Lemma l_exists_reduce

∀[T:Type]. ∀L:T List. ∀P:T ⟶ 𝔹.  ((∃x∈L. ↑P[x]) ⇐⇒ ↑reduce(λx,y. (P[x] ∨by);ff;L))
BY
{ ((RepeatFor 2 (D 0 THENA Auto) THEN ListInd (-1)) THEN Reduce 0) }

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

2
1. [T] : Type
2. u : T
3. v : T List
4. ∀P:T ⟶ 𝔹. ((∃x∈v. ↑P[x]) ⇐⇒ ↑reduce(λx,y. (P[x] ∨by);ff;v))
⊢ ∀P:T ⟶ 𝔹. ((∃x∈[u / v]. ↑P[x]) ⇐⇒ ↑(P[u] ∨breduce(λx,y. (P[x] ∨by);ff;v)))

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}L:T  List.  \mforall{}P:T  {}\mrightarrow{}  \mBbbB{}.    ((\mexists{}x\mmember{}L.  \muparrow{}P[x])  \mLeftarrow{}{}\mRightarrow{}  \muparrow{}reduce(\mlambda{}x,y.  (P[x]  \mvee{}\msubb{}y);ff;L))


By

---

Latex:
((RepeatFor  2  (D  0  THENA  Auto)  THEN  ListInd  (-1))  THEN  Reduce  0)

---

Home Index