---

Step * 2 1 of Lemma length-filter-decreases

.....antecedent..... 
1. T : Type
2. P : T ⟶ 𝔹
3. u : T
4. v : T List
5. ↑(P u)
6. (∃x∈[u / v]. ¬↑(P x))
⊢ (∃x∈v. ¬↑(P x))
BY
{ D (-1) }

1
1. T : Type
2. P : T ⟶ 𝔹
3. u : T
4. v : T List
5. ↑(P u)
6. i : ℕ||[u / v]||
7. ¬↑(P [u / v][i])
⊢ (∃x∈v. ¬↑(P x))

---

Latex:

---

Latex:
.....antecedent..... 
1.  T  :  Type
2.  P  :  T  {}\mrightarrow{}  \mBbbB{}
3.  u  :  T
4.  v  :  T  List
5.  \muparrow{}(P  u)
6.  (\mexists{}x\mmember{}[u  /  v].  \mneg{}\muparrow{}(P  x))
\mvdash{}  (\mexists{}x\mmember{}v.  \mneg{}\muparrow{}(P  x))


By

---

Latex:
D  (-1)

---

Home Index